Commit 2026-07-27 15:11 a76bb818

View on Github →

feat(Algebra/Algebra): reinterpret a RingEquiv as a ℕ/ℤ/ℚ-algebra isomorphism (#40298) Adds the RingEquiv analogues of the RingHom.to{Nat,Int,Rat}AlgHom / RingHom.equivRatAlgHom constructions, over ℕ, ℤ and ℚ:

RingEquiv.toNatAlgEquiv, RingEquiv.toIntAlgEquiv, RingEquiv.toRatAlgEquiv: a RingEquiv is canonically an ℕ-, ℤ- or ℚ-algebra isomorphism.
ringEquivEquivNatAlgEquiv, ringEquivEquivIntAlgEquiv, ringEquivEquivRatAlgEquiv: the corresponding equivalences (R ≃+* S) ≃ (R ≃ₐ[·] S). :robot: This PR was extracted from the SKW project by Claude.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem RingEquiv.coe_toIntAlgEquiv

added theorem RingEquiv.coe_toNatAlgEquiv

added def RingEquiv.equivIntAlgEquiv

added def RingEquiv.equivNatAlgEquiv

added theorem RingEquiv.symm_toIntAlgEquiv

added theorem RingEquiv.symm_toNatAlgEquiv

added theorem RingEquiv.toAlgHom_toIntAlgEquiv

added theorem RingEquiv.toAlgHom_toNatAlgEquiv

added def RingEquiv.toIntAlgEquiv

added theorem RingEquiv.toIntAlgEquiv_injective

added def RingEquiv.toNatAlgEquiv

added theorem RingEquiv.toNatAlgEquiv_injective

Modified Mathlib/Algebra/Algebra/Hom/Rat.lean

added theorem AlgEquiv.toRatAlgEquiv_toRingEquiv

modified theorem AlgHom.toRingHom_toRatAlgHom

added theorem RingEquiv.coe_toRatAlgEquiv

added def RingEquiv.equivRatAlgEquiv

added theorem RingEquiv.symm_toRatAlgEquiv

added theorem RingEquiv.toAlgHom_toRatAlgEquiv

added def RingEquiv.toRatAlgEquiv

added theorem RingEquiv.toRatAlgEquiv_injective

added theorem RingEquiv.toRingEquiv_toRatAlgEquiv

modified def RingHom.equivRatAlgHom

modified def RingHom.toRatAlgHom

modified theorem RingHom.toRatAlgHom_apply

modified theorem RingHom.toRatAlgHom_toRingHom