traceDual_top — Mathlib

English

The dual of the bottom submodule is the top submodule: (⊥)ᵛ = ⊤.

Русский

Дуальность по следу нижнего подмодуля равна верхнему: (⊥)ᵛ = ⊤.

LaTeX

$$$(\bot)^{\\vee} = \\top$$$

Lean4

theorem traceDual_top [Decidable (IsField A)] : (⊤ : Submodule B L)ᵛ = if IsField A then ⊤ else ⊥ :=
  by
  convert traceDual_top'
  rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
    LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L), ← RingHom.range_eq_top, _root_.eq_top_iff]
  simp [SetLike.le_def]

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