Commit 2023-08-03 04:09 966fdb63

View on Github →

chore: flip and rename rank_eq_of_injective (#6301)

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

deleted theorem rank_eq_of_injective

added theorem rank_range_of_injective

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean