quotDualEquivAnnihilator — Mathlib

English

The quotient by the dual equals the dual annihilator via a natural equivalence.

Русский

Картезиев переход: квотирование по дуалу дает дуальный аннигилятор через естественное соответствие.

LaTeX

$$quotDualEquivAnnihilator (W) : (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] W.dualAnnihilator$$

Lean4

/-- The quotient by the dual is isomorphic to its dual annihilator. -/
noncomputable def quotDualEquivAnnihilator (W : Subspace K V) :
    (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] W.dualAnnihilator :=
  LinearEquiv.quotEquivOfQuotEquiv <| LinearEquiv.trans W.quotAnnihilatorEquiv W.dualEquivDual

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