zero_mem_smul_iff — Mathlib

English

For NoZeroSMulDivisors α β, the zero element is in the product set exactly when one factor contains zero and the other is nonempty.

Русский

Для NoZeroSMulDivisors α β ноль в произведении множеств s • t встречается тогда, когда одно из множеств содержит ноль, а другое непусто.

LaTeX

$$$0 \in s \cdot t \iff (0 \in s \land t \neq \varnothing) \lor (0 \in t \land s \neq \varnothing)$$$

Lean4

theorem zero_mem_smul_iff : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
    where
  mp := by
    rintro ⟨a, ha, b, hb, h⟩
    obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h
    · exact Or.inl ⟨ha, b, hb⟩
    · exact Or.inr ⟨hb, a, ha⟩
  mpr := by
    rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact ⟨0, hs, b, hb, zero_smul _ _⟩
    · exact ⟨a, ha, 0, ht, smul_zero _⟩

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