Theorems · Theorem · linear algebra

Matrix.IsPivotedBy.rank_eq

∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : LinearOrder m]
  [inst_3 : LinearOrder n] [inst_4 : CommRing R] [IsDomain R] {A : Matrix m n R} {l : m → WithTop n},
  A.IsPivotedBy l → A.rank = {i | l i ≠ ⊤}.card

Defined in: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Cited by: 1 results in Mathlib
Foundations: Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype Fintype LinearOrder LinearOrder CommRing IsDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites34

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Top.topstatement and proof · cited by 9,680
LinearOrderstatement and proof · cited by 8,572
SetLike.coeproof · cited by 8,199
Fintypestatement and proof · cited by 7,736
Set.ofPredproof · cited by 6,101
Matrixstatement and proof · cited by 4,303
WithTopstatement and proof · cited by 3,754
Finset.univstatement and proof · cited by 3,473
Finset.cardstatement and proof · cited by 2,327
IsDomainstatement and proof · cited by 2,196
le_antisymmproof · cited by 2,068

Cited by1

Results whose statement or proof uses this declaration.

Echelon.Decomposition.rank_eqproof · cited by 0