Commit 2024-10-03 05:41 491935d5

View on Github →

chore: unify monotonicity of rank lemmas (#17292) The names were all over the place. Rename:

rank_le_of_submodule -> Submodule.rank_mono
Submodule.finrank_le_finrank_of_le -> Submodule.finrank_mono (existing, up to unfolding Monotone)
rank_submodule_le -> Submodule.rank_le From LeanCamCombi

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem Submodule.rank_le

added theorem Submodule.rank_mono

deleted theorem rank_le_of_submodule

deleted theorem rank_submodule_le

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

deleted theorem Submodule.finrank_le_finrank_of_le

added theorem Submodule.finrank_mono

Modified Mathlib/LinearAlgebra/Dimension/LinearMap.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

deleted theorem Submodule.finrank_mono

Modified Mathlib/LinearAlgebra/LinearDisjoint.lean