noZeroSMulDivisors — Mathlib

English

If α has zero, each f i has zero, SMulWithZero α (f i) and NoZeroSMulDivisors α (f i) for all i, then NoZeroSMulDivisors α (∀ i, f i).

Русский

Если для каждой i множество f(i) имеет ноль и выполнено свойство NoZeroSMulDivisors α (f i) и SMulWithZero α (f i), то NoZeroSMulDivisors α (i → f i).

LaTeX

$$$$\forall i, NoZeroSMulDivisors(\alpha, f(i)) \implies NoZeroSMulDivisors(\alpha, (i \mapsto f(i))).$$$$

Lean4

instance noZeroSMulDivisors (α) [Zero α] [∀ i, Zero <| f i] [∀ i, SMulWithZero α <| f i]
    [∀ i, NoZeroSMulDivisors α <| f i] : NoZeroSMulDivisors α (∀ i : I, f i) :=
  ⟨fun {_ _} h => or_iff_not_imp_left.mpr fun hc => funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩

Похожие утверждения