English
If α, β have no zero-divisors with respect to the scalar action and NoZeroSMulDivisors α β holds, then NoZeroSMulDivisors α (Set β) also holds; the zero-product property for scalars lifts to sets.
Русский
Если выполняются условия без нулевых делителей для скалярного действия и NoZeroSMulDivisors α β, то NoZeroSMulDivisors α (Set β) также верно; свойство нулевого произведения поднимается до множеств.
LaTeX
$$$ \forall [Zero \ α] [Zero \ β] [SMul \ α \ β] [NoZeroSMulDivisors \ α \ β], NoZeroSmulDivisors (Set α) (Set β).$$$
Lean4
instance instNoZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
NoZeroSMulDivisors (Set α) (Set β) where
eq_zero_or_eq_zero_of_smul_eq_zero {s t}
h := by
by_contra! H
have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H
simp only [not_subset, mem_zero] at H
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul hs ht).elim ha hb
