dualAnnihilator_eq_bot_iff' — Mathlib

English

The dual annihilator W.dualAnnihilator equals the zero subspace if and only if the dual space of the quotient is subsingleton.

Русский

Двойной аннигилятор W.dualAnnihilator равен нулевому подпространству тогда и только тогда, когда двойственное пространство фактора является единичным.

LaTeX

$$W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W))$$

Lean4

theorem dualAnnihilator_eq_bot_iff' {W : Submodule R M} : W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W)) := by
  rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]

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