Theorem rankCondition_iff_le_of_comp_eq_one

Modification history

2025-12-28 17:51
Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean
feat(Algebra): stably finite rings (#32262) …
Added rankCondition_iff_le_of_comp_eq_oneView on Github →