Theorem LinearMap.finrank_le_of_isSMulRegular

Modification history

2024-11-23 13:41
Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
chore: rename *of_smul_regular lemmas (#19326)
Added LinearMap.finrank_le_of_isSMulRegularView on Github →