prod_eq_bot_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_eq_bot_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} : p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥ := by
  simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot, ker_inl, ker_inr]

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