quotient_prod_linearEquiv — Mathlib

English

For any submodule p of V, there exists a linear isomorphism between V and (V/p) × p.

Русский

Для любого подподпространства p в V существует линейное изоморфизм V ≅ (V / p) × p.

LaTeX

$$$\exists \phi:\; ((V / p) \times p) \cong_K V$$$

Lean4

theorem quotient_prod_linearEquiv (p : Submodule K V) : Nonempty (((V ⧸ p) × p) ≃ₗ[K] V) :=
  let ⟨q, hq⟩ := p.exists_isCompl
  Nonempty.intro <|
    ((quotientEquivOfIsCompl p q hq).prodCongr (LinearEquiv.refl _ _)).trans (prodEquivOfIsCompl q p hq.symm)

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