Theorem LinearMap.finrank_le_of_smul_regular

Modification history

2024-11-23 13:41

Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

chore: rename *of_smul_regular lemmas (#19326)

Deleted LinearMap.finrank_le_of_smul_regular View on Github →

2024-11-20 20:34

Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span (#18569) …

Added LinearMap.finrank_le_of_smul_regular View on Github →