Pi instances for NoZeroSMulDivisors #
This file defines instances for NoZeroSMulDivisors on Pi types.
instance
Pi.noZeroSMulDivisors
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[Semiring α]
[IsDomain α]
[(i : I) → AddCommGroup (f i)]
[(i : I) → Module α (f i)]
[∀ (i : I), NoZeroSMulDivisors α (f i)]
:
NoZeroSMulDivisors α ((i : I) → f i)
instance
Function.noZeroSMulDivisors
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Semiring α]
[IsDomain α]
[AddCommGroup β]
[Module α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (ι → β)
A special case of Pi.noZeroSMulDivisors for non-dependent types. Lean struggles to
synthesize this instance by itself elsewhere in the library.