Commit 2025-02-20 18:07 0acb8bef

View on Github →

chore: rename Injective.sum_elim and friends (#22129) Per the naming convention, they should be written sumElim, etc.

Estimated changes

Modified Mathlib/Data/Countable/Basic.lean

Modified Mathlib/Data/Sum/Basic.lean

added theorem Function.Bijective.sumMap

deleted theorem Function.Bijective.sum_map

added theorem Function.Injective.sumElim

added theorem Function.Injective.sumMap

deleted theorem Function.Injective.sum_elim

deleted theorem Function.Injective.sum_map

added theorem Function.Surjective.sumMap

deleted theorem Function.Surjective.sum_map

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/Homeomorph.lean