rank_of_isUnit — Mathlib

English

If A is invertible (det A is a unit, equivalently A is invertible), then rank(A) = n.

Русский

Если A обратима (det A единица или есть обратная матрица), то ранг(A) = n.

LaTeX

$$$\text{If } A \in M_{n\times n}(R) \text{ is invertible, then } \operatorname{rank}(A) = n$$$

Lean4

theorem rank_of_isUnit [Nontrivial R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) : A.rank = Fintype.card n :=
  by
  obtain ⟨A, rfl⟩ := h
  exact rank_unit A

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