Commit 2025-06-09 16:45 3c689580

View on Github →

fix: Remove lemmas from Ring/Hom/Basic (#25447) Removes extraneous lemmas from Ring/Hom/Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Equiv/TransferInstance.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Ring/Hom/Basic.lean

deleted theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero

Created Mathlib/Algebra/Ring/Hom/InjSurj.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.range_const

added theorem Set.range_eq_singleton

added theorem Set.range_eq_singleton_iff

Created Mathlib/Deprecated/RingHom.lean

added theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Content.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean