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)
[Zero α]
[(i : I) → Zero (f i)]
[(i : I) → SMulWithZero α (f i)]
[∀ (i : I), NoZeroSMulDivisors α (f i)]
:
NoZeroSMulDivisors α ((i : I) → f i)
instance
Function.noZeroSMulDivisors
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (ι → β)
A special case of Pi.noZeroSMulDivisors for non-dependent types. Lean struggles to
synthesize this instance by itself elsewhere in the library.