Theorem RingHom.toRatAlgHom_apply

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.toRatAlgHom_applyView on Github →
2025-03-11 07:07
Mathlib/Algebra/Algebra/Hom/Rat.lean
chore: review of `erw` in `NumberTheory/` (#22813)
Added RingHom.toRatAlgHom_applyView on Github →