prod_eq_top_iff — Mathlib

English

For submodules p1 ⊆ M and p2 ⊆ M′, their product is top if and only if both p1 and p2 are top.

Русский

Для подмодулов p1 ⊆ M и p2 ⊆ M′ их произведение равно верхнему тогда, когда оба подмодуля равны верхнему.

LaTeX

$$$p_1.\mathrm{prod} p_2 = \top \iff p_1 = \top \land p_2 = \top$$$

Lean4

theorem prod_eq_top_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} : p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤ := by
  simp only [eq_top_iff, le_prod_iff, map_top, range_fst, range_snd]

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