hasRankNullity — Mathlib

English

There exists a rank-nullity framework for linear maps over division rings; in particular, a rank-nullity decomposition exists for appropriate structures.

Русский

Существуют разложения по рангу и нулю для линейных отображений над делением колец; в частности существует соответствующее разложение.

LaTeX

$$HasRankNullity_K$$

Lean4

instance hasRankNullity : HasRankNullity.{u₀} K
    where
  rank_quotient_add_rank := rank_quotient_add_rank_of_divisionRing
  exists_set_linearIndependent V _
    _ := by
    let b := Module.Free.chooseBasis K V
    refine ⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩
    rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective, Module.Free.rank_eq_card_chooseBasisIndex]

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