Commit 2026-06-19 13:16 63c85da7

View on Github →

chore: rename Pi.algHom to AlgHom.pi (#40044)

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

added def AlgHom.pi

added theorem AlgHom.pi_comp

added theorem AlgHom.pi_evalAlgHom

deleted def Pi.algHom

added theorem Pi.algHom_apply

deleted theorem Pi.algHom_evalAlgHom

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

modified theorem Polynomial.aeval_pi

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/RingTheory/RingHom/QuasiFinite.lean

Modified Mathlib/RingTheory/Smooth/Pi.lean

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