Theorem AlgHom.toRingHom_toRatAlgHom

Modification history

2026-07-27 15:11
Mathlib/Algebra/Algebra/Hom/Rat.lean
feat(Algebra/Algebra): reinterpret a RingEquiv as a ℕ/ℤ/ℚ-algebra isomorphism (#40298) …
Modified AlgHom.toRingHom_toRatAlgHomView on Github →
2024-07-17 12:28
Mathlib/Algebra/Algebra/Hom.lean
chore (Algebra.Basic): split results on `Algebra`'s over `Rat` to a separate file (#14567) …
Modified AlgHom.toRingHom_toRatAlgHomView on Github →
2023-02-21 08:05
Mathlib/Algebra/Algebra/Hom.lean
feat: port Algebra.Algebra.Hom (#2371)
Added AlgHom.toRingHom_toRatAlgHomView on Github →