Def RingHom.toIntAlgHom

Modification history

2024-09-14 03:36

Mathlib/Algebra/Algebra/Hom.lean

feat(Algebra/Algebra/Hom): add lemmas about toNatAlgHom and toIntAlgHom (#16790)

Modified RingHom.toIntAlgHom View on Github →

2023-02-21 08:05

Mathlib/Algebra/Algebra/Hom.lean

feat: port Algebra.Algebra.Hom (#2371)

Added RingHom.toIntAlgHom View on Github →