noZeroSMulDivisors_set — Mathlib

English

The NoZeroSMulDivisors property for Set β propagates through the Set-level action as a simp lemma, mirroring the scalar case.

Русский

Свойство NoZeroSMulDivisors для Set β сохраняется в уровне действий над множествами и содержит симп-лемму такого типа.

LaTeX

$$$ \text{NoZeroSMulDivisors } \alpha (Set \beta) $$$

Lean4

instance noZeroSMulDivisors_set [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Set β)
    where
  eq_zero_or_eq_zero_of_smul_eq_zero {a s}
    h := by
    by_contra! H
    have hst : (a • s).Nonempty := h.symm.subst zero_nonempty
    rw [Ne, Ne, ← hst.of_image.subset_zero_iff, not_subset] at H
    obtain ⟨ha, b, ht, hb⟩ := H
    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul_set ht).elim ha hb

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