rank_unit — Mathlib

English

If A is invertible in the n×n matrix ring over R, then rank(A) = n.

Русский

Если A обратима в кольце матриц размером n×n над R, то ранг(A) = n.

LaTeX

$$$A \in (M_{n\times n}(R))^{\times} \implies \operatorname{rank}(A) = n$$$

Lean4

theorem rank_unit [Nontrivial R] [DecidableEq n] (A : (Matrix n n R)ˣ) : (A : Matrix n n R).rank = Fintype.card n :=
  by
  apply le_antisymm (rank_le_card_width (A : Matrix n n R)) _
  have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
  rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this

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