Def RingHom.equivRatAlgHom

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 RingHom.equivRatAlgHomView 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 RingHom.equivRatAlgHomView on Github →
2024-05-17 19:31
Mathlib/Algebra/Algebra/Hom.lean
style: remove all isolated `where` (#12991)
Modified RingHom.equivRatAlgHomView on Github →
2023-02-21 08:05
Mathlib/Algebra/Algebra/Hom.lean
feat: port Algebra.Algebra.Hom (#2371)
Added RingHom.equivRatAlgHomView on Github →