Commit 2024-11-23 13:41 53fa3b7d

View on Github →

chore: rename *of_smul_regular lemmas (#19326)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem rank_le_of_isSMulRegular

deleted theorem rank_le_of_smul_regular

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

added theorem LinearMap.finrank_le_of_isSMulRegular

deleted theorem LinearMap.finrank_le_of_smul_regular

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean