Commit 2025-01-28 11:07 fb4aed52

View on Github →

chore: delete deprecated algebraic structure files (#16836) Based on a comparison with 32de3f675e28bc8b32de22cba2660940d0a5fc10 these six files have not been substantially changed for over a year.

Estimated changes

deleted theorem Additive.isAddGroupHom
deleted theorem Additive.isAddHom
deleted theorem Additive.isAddMonoidHom
deleted theorem Inv.isGroupHom
deleted theorem IsAddGroupHom.sub
deleted structure IsAddGroupHom
deleted structure IsAddHom
deleted structure IsAddMonoidHom
deleted theorem IsGroupHom.comp
deleted theorem IsGroupHom.id
deleted theorem IsGroupHom.injective_iff
deleted theorem IsGroupHom.inv
deleted theorem IsGroupHom.map_div
deleted theorem IsGroupHom.map_inv
deleted theorem IsGroupHom.map_mul'
deleted theorem IsGroupHom.map_one
deleted theorem IsGroupHom.mk'
deleted theorem IsGroupHom.mul
deleted theorem IsGroupHom.to_isMonoidHom
deleted structure IsGroupHom
deleted theorem IsMonoidHom.comp
deleted theorem IsMonoidHom.id
deleted theorem IsMonoidHom.inv
deleted theorem IsMonoidHom.map_mul'
deleted structure IsMonoidHom
deleted theorem IsMulHom.comp
deleted theorem IsMulHom.id
deleted theorem IsMulHom.inv
deleted theorem IsMulHom.mul
deleted theorem IsMulHom.to_isMonoidHom
deleted structure IsMulHom
deleted theorem IsUnit.map'
deleted theorem MonoidHom.coe_of
deleted theorem MonoidHom.isGroupHom
deleted theorem MonoidHom.isMonoidHom_coe
deleted def MonoidHom.of
deleted theorem MulEquiv.isGroupHom
deleted theorem MulEquiv.isMonoidHom
deleted theorem MulEquiv.isMulHom
deleted theorem Multiplicative.isGroupHom
deleted theorem Multiplicative.isMulHom
deleted theorem RingHom.to_isAddGroupHom
deleted theorem RingHom.to_isAddMonoidHom
deleted theorem RingHom.to_isMonoidHom
deleted theorem Units.coe_isMonoidHom
deleted theorem Units.coe_map'
deleted theorem IsRingHom.comp
deleted theorem IsRingHom.id
deleted theorem IsRingHom.map_neg
deleted theorem IsRingHom.map_sub
deleted theorem IsRingHom.map_zero
deleted theorem IsRingHom.of_semiring
deleted structure IsRingHom
deleted theorem IsSemiringHom.comp
deleted theorem IsSemiringHom.id
deleted structure IsSemiringHom
deleted theorem RingHom.coe_of
deleted def RingHom.of
deleted theorem RingHom.to_isRingHom
deleted theorem RingHom.to_isSemiringHom
deleted theorem Field.closure.isSubfield
deleted theorem Field.closure.isSubmonoid
deleted def Field.closure
deleted theorem Field.closure_mono
deleted theorem Field.closure_subset
deleted theorem Field.closure_subset_iff
deleted theorem Field.mem_closure
deleted theorem Field.ring_closure_subset
deleted theorem Field.subset_closure
deleted theorem Image.isSubfield
deleted theorem IsSubfield.div_mem
deleted theorem IsSubfield.iInter
deleted theorem IsSubfield.inter
deleted theorem IsSubfield.pow_mem
deleted structure IsSubfield
deleted theorem Preimage.isSubfield
deleted theorem Range.isSubfield
deleted theorem Univ.isSubfield
deleted inductive AddGroup.InClosure
deleted theorem Additive.isAddSubgroup
deleted inductive Group.InClosure
deleted theorem Group.closure.isSubgroup
deleted def Group.closure
deleted theorem Group.closure_eq_mclosure
deleted theorem Group.closure_mono
deleted theorem Group.closure_subgroup
deleted theorem Group.closure_subset
deleted theorem Group.closure_subset_iff
deleted theorem Group.conjugatesOf_subset
deleted theorem Group.image_closure
deleted theorem Group.mclosure_inv_subset
deleted theorem Group.mclosure_subset
deleted theorem Group.mem_closure
deleted def Group.normalClosure
deleted theorem Group.normalClosure_mono
deleted theorem Group.subset_closure
deleted theorem IsAddSubgroup.of_sub
deleted structure IsAddSubgroup
deleted theorem IsGroupHom.image_subgroup
deleted theorem IsGroupHom.inv_iff_ker'
deleted theorem IsGroupHom.inv_iff_ker
deleted theorem IsGroupHom.inv_ker_one'
deleted theorem IsGroupHom.inv_ker_one
deleted def IsGroupHom.ker
deleted theorem IsGroupHom.mem_ker
deleted theorem IsGroupHom.one_ker_inv'
deleted theorem IsGroupHom.one_ker_inv
deleted theorem IsGroupHom.preimage
deleted theorem IsGroupHom.range_subgroup
deleted structure IsNormalAddSubgroup
deleted structure IsNormalSubgroup
deleted def IsSubgroup.center
deleted theorem IsSubgroup.center_normal
deleted theorem IsSubgroup.div_mem
deleted theorem IsSubgroup.eq_trivial_iff
deleted theorem IsSubgroup.iInter
deleted theorem IsSubgroup.inter
deleted theorem IsSubgroup.inv_mem_iff
deleted theorem IsSubgroup.mem_center
deleted theorem IsSubgroup.mem_norm_comm
deleted theorem IsSubgroup.mem_trivial
deleted theorem IsSubgroup.of_div
deleted def IsSubgroup.trivial
deleted theorem IsSubgroup.trivial_normal
deleted theorem IsSubgroup.univ_subgroup
deleted structure IsSubgroup
deleted theorem Multiplicative.isSubgroup
deleted theorem Subgroup.isSubgroup
deleted def Subgroup.of
deleted theorem Subgroup.of_normal
deleted inductive AddMonoid.InClosure
deleted theorem Additive.isAddSubmonoid
deleted structure IsAddSubmonoid
deleted theorem IsSubmonoid.iInter
deleted theorem IsSubmonoid.image
deleted theorem IsSubmonoid.inter
deleted theorem IsSubmonoid.list_prod_mem
deleted theorem IsSubmonoid.pow_mem
deleted theorem IsSubmonoid.powers_subset
deleted theorem IsSubmonoid.preimage
deleted structure IsSubmonoid
deleted def Monoid.Closure
deleted inductive Monoid.InClosure
deleted theorem Monoid.closure_mono
deleted theorem Monoid.closure_singleton
deleted theorem Monoid.closure_subset
deleted theorem Monoid.image_closure
deleted theorem Monoid.subset_closure
deleted theorem Range.isSubmonoid
deleted theorem Submonoid.isSubmonoid
deleted def Submonoid.of
deleted theorem Univ.isSubmonoid
deleted theorem powers.isSubmonoid
deleted theorem powers.mul_mem
deleted theorem powers.one_mem
deleted theorem powers.self_mem
deleted def powers
deleted theorem IsSubring.iInter
deleted theorem IsSubring.inter
deleted def IsSubring.subring
deleted structure IsSubring
deleted theorem Ring.closure.isSubring
deleted def Ring.closure
deleted theorem Ring.closure_mono
deleted theorem Ring.closure_subset
deleted theorem Ring.closure_subset_iff
deleted theorem Ring.image_closure
deleted theorem Ring.mem_closure
deleted theorem Ring.subset_closure
deleted theorem RingHom.isSubring_image