Commit 2023-01-06 08:41 6df3ab72

View on Github →

feat: Port Deprecated.Group and Deprecated.Ring (#1368)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/Group.lean

added theorem Additive.isAddGroupHom

added theorem Additive.isAddHom

added theorem Additive.isAddMonoidHom

added theorem Inv.isGroupHom

added theorem IsAddGroupHom.sub

added structure IsAddGroupHom

added structure IsAddHom

added theorem IsAddMonoidHom.isAddMonoidHom_mul_left

added theorem IsAddMonoidHom.isAddMonoidHom_mul_right

added structure IsAddMonoidHom

added theorem IsGroupHom.comp

added theorem IsGroupHom.id

added theorem IsGroupHom.injective_iff

added theorem IsGroupHom.inv

added theorem IsGroupHom.map_div

added theorem IsGroupHom.map_inv

added theorem IsGroupHom.map_mul'

added theorem IsGroupHom.map_one

added theorem IsGroupHom.mk'

added theorem IsGroupHom.mul

added theorem IsGroupHom.to_isMonoidHom

added structure IsGroupHom

added theorem IsMonoidHom.comp

added theorem IsMonoidHom.id

added theorem IsMonoidHom.inv

added theorem IsMonoidHom.map_mul'

added structure IsMonoidHom

added theorem IsMulHom.comp

added theorem IsMulHom.id

added theorem IsMulHom.inv

added theorem IsMulHom.mul

added theorem IsMulHom.to_isMonoidHom

added structure IsMulHom

added theorem IsUnit.map'

added theorem MonoidHom.coe_of

added theorem MonoidHom.isGroupHom

added theorem MonoidHom.isMonoidHom_coe

added def MonoidHom.of

added theorem MulEquiv.isGroupHom

added theorem MulEquiv.isMonoidHom

added theorem MulEquiv.isMulHom

added theorem Multiplicative.isGroupHom

added theorem Multiplicative.isMonoidHom

added theorem Multiplicative.isMulHom

added theorem RingHom.to_isAddGroupHom

added theorem RingHom.to_isAddMonoidHom

added theorem RingHom.to_isMonoidHom

added theorem Units.coe_isMonoidHom

added theorem Units.coe_map'

added def Units.map'

Created Mathlib/Deprecated/Ring.lean

added theorem IsRingHom.comp

added theorem IsRingHom.id

added theorem IsRingHom.map_neg

added theorem IsRingHom.map_sub

added theorem IsRingHom.map_zero

added theorem IsRingHom.of_semiring

added theorem IsRingHom.to_isAddGroupHom

added theorem IsRingHom.to_isSemiringHom

added structure IsRingHom

added theorem IsSemiringHom.comp

added theorem IsSemiringHom.id

added theorem IsSemiringHom.to_isAddMonoidHom

added theorem IsSemiringHom.to_isMonoidHom

added structure IsSemiringHom

added theorem RingHom.coe_of

added def RingHom.of

added theorem RingHom.to_isRingHom

added theorem RingHom.to_isSemiringHom