Commit 2024-09-14 03:36 784d6209

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

modified def RingHom.toIntAlgHom

added theorem RingHom.toIntAlgHom_apply

added theorem RingHom.toIntAlgHom_coe

modified theorem RingHom.toIntAlgHom_injective

added theorem RingHom.toNatAlgHom_apply

added theorem RingHom.toNatAlgHom_coe