quotEquivOfQuotEquiv — Mathlib

English

If there exists a linear equivalence f: V/p ≃ q, then there is a linear equivalence (V/q) ≃ p.

Русский

Если существует линейное эквивалентное отображение f: V/p ≃ q, то существует линейное эквивалентное отображение (V/q) ≃ p.

LaTeX

$$Given f : (V ⧸ p) ≃ q, then (V ⧸ q) ≃ p$$

Lean4

/-- Given the subspaces `p q`, if `p.quotient ≃ₗ[K] q`, then `q.quotient ≃ₗ[K] p` -/
noncomputable def quotEquivOfQuotEquiv {p q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] q) : (V ⧸ q) ≃ₗ[K] p :=
  LinearEquiv.ofFinrankEq _ _ <| by
    rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f, add_comm,
      Submodule.finrank_quotient_add_finrank]

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