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)

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯