Theorems · Theorem · linear algebra

Matrix.rank_mul_eq_right_of_isLowerTriangular

∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype m]
  [inst_4 : LinearOrder m] (A : Matrix m m R) (B : Matrix m n R),
  A.IsLowerTriangular → (∀ (i : m), A.diag i ≠ 0) → (A * B).rank = B.rank

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

1 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeCommRingIsDomainFintypeLinearOrder