dualAnnihilator_top — Mathlib

English

The dual annihilator of the top submodule is the bottom submodule.

Русский

Дуальный аннигилирующий подмодуль верха равен нулю.

LaTeX

$$Submodule.dualAnnihilator_top : (⊤ : Submodule R M).dualAnnihilator = ⊥$$

Lean4

@[simp]
theorem dualAnnihilator_top : (⊤ : Submodule R M).dualAnnihilator = ⊥ :=
  by
  rw [eq_bot_iff]
  intro v
  simp_rw [mem_dualAnnihilator, mem_bot, mem_top, forall_true_left]
  exact fun h => LinearMap.ext h

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