Commit 2024-11-13 05:12 b71606a9

View on Github →

chore: rename lemmas to range_eq_top/range_eq_top_of_surjective (#18853) Many lemmas are called range_top_iff_surjective, and then there is LinearMap.range_eq_top, LieHom.range_eq_top, LieModuleHom.range_eq_top. Unify the lemma names by renaming them all to range_eq_top_iff_surjective

Estimated changes

added theorem AlgHom.range_eq_top
added theorem MonoidHom.range_eq_top
modified theorem LinearMap.range_eq_top
added theorem RingHom.range_eq_top
added theorem Set.range_eq_univ
deleted theorem Set.range_iff_surjective
modified theorem QuotientGroup.range_mk