Commit 2026-05-30 14:32 f3c1871f

View on Github →

chore: rename Pi.ringHom to RingHom.pi (#40039) Discussed on Zulip at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Pi.2EfooHom.20or.20FooHom.2Epi/near/598538630

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/Algebra/Category/Ring/Under/Limits.lean

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

Modified Mathlib/Algebra/Ring/Pi.lean

added def NonUnitalRingHom.pi

added theorem NonUnitalRingHom.pi_injective

deleted theorem Pi.nonUnitalRingHom_injective

deleted theorem Pi.ringHom_injective

added theorem RingHom.pi_injective

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/PointsPi.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

modified def NumberField.canonicalEmbedding

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/Pure.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Modified Mathlib/RingTheory/Idempotents.lean

Modified Mathlib/RingTheory/Localization/Pi.lean

Modified Mathlib/RingTheory/Spectrum/Maximal/Localization.lean