finiteDimensional_quot_dualCoannihilator_iff

English

For W ⊆ V dual space, finite dimensional has equivalence between finiteness of V/W.dualCoannihilator and finiteness of W.

Русский

Для W ⊆ V дуальное пространство, конечномерность V/W.dualCoannihilator эквивалентна конечномерности W.

LaTeX

$$$\\text{FiniteDimensional}(V/W.dualCoannihilator) \\iff \\text{FiniteDimensional}(W)$$$

Lean4

theorem finiteDimensional_quot_dualCoannihilator_iff {W : Submodule K (Dual K V)} :
    FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K W :=
  ⟨fun _ ↦ FiniteDimensional.of_injective _ W.flip_quotDualCoannihilatorToDual_injective, fun _ ↦
    FiniteDimensional.of_injective _ W.quotDualCoannihilatorToDual_injective⟩

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