Theorem RingHom.toIntAlgHom_coe

Modification history

2024-09-14 03:36

Mathlib/Algebra/Algebra/Hom.lean

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

Added RingHom.toIntAlgHom_coe View on Github →