Commit 2023-01-27 13:20 5ed72b2b

View on Github →

feat: port Deprecated.Subgroup (#1876)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/Subgroup.lean

added inductive AddGroup.InClosure

added theorem Additive.isAddSubgroup

added theorem Additive.isAddSubgroup_iff

added theorem Additive.isNormalAddSubgroup

added theorem Additive.isNormalAddSubgroup_iff

added inductive Group.InClosure

added theorem Group.closure.isSubgroup

added def Group.closure

added theorem Group.closure_eq_mclosure

added theorem Group.closure_mono

added theorem Group.closure_subgroup

added theorem Group.closure_subset

added theorem Group.closure_subset_iff

added theorem Group.conjugatesOfSet_subset'

added theorem Group.conjugatesOfSet_subset_normalClosure

added theorem Group.conjugatesOf_subset

added theorem Group.exists_list_of_mem_closure

added theorem Group.image_closure

added theorem Group.mclosure_inv_subset

added theorem Group.mclosure_subset

added theorem Group.mem_closure

added theorem Group.mem_closure_union_iff

added theorem Group.normalClosure.isSubgroup

added theorem Group.normalClosure.is_normal

added def Group.normalClosure

added theorem Group.normalClosure_mono

added theorem Group.normalClosure_subset

added theorem Group.normalClosure_subset_iff

added theorem Group.subset_closure

added theorem Group.subset_normalClosure

added theorem IsAddSubgroup.of_sub

added structure IsAddSubgroup

added theorem IsGroupHom.image_subgroup

added theorem IsGroupHom.injective_iff_trivial_ker

added theorem IsGroupHom.injective_of_trivial_ker

added theorem IsGroupHom.inv_iff_ker'

added theorem IsGroupHom.inv_iff_ker

added theorem IsGroupHom.inv_ker_one'

added theorem IsGroupHom.inv_ker_one

added theorem IsGroupHom.isNormalSubgroup_ker

added def IsGroupHom.ker

added theorem IsGroupHom.mem_ker

added theorem IsGroupHom.one_iff_ker_inv'

added theorem IsGroupHom.one_iff_ker_inv

added theorem IsGroupHom.one_ker_inv'

added theorem IsGroupHom.one_ker_inv

added theorem IsGroupHom.preimage

added theorem IsGroupHom.preimage_normal

added theorem IsGroupHom.range_subgroup

added theorem IsGroupHom.trivial_ker_iff_eq_one

added theorem IsGroupHom.trivial_ker_of_injective

added structure IsNormalAddSubgroup

added structure IsNormalSubgroup

added def IsSubgroup.center

added theorem IsSubgroup.center_normal

added theorem IsSubgroup.div_mem

added theorem IsSubgroup.eq_trivial_iff

added theorem IsSubgroup.inter

added theorem IsSubgroup.interᵢ

added theorem IsSubgroup.inv_mem_iff

added theorem IsSubgroup.mem_center

added theorem IsSubgroup.mem_norm_comm

added theorem IsSubgroup.mem_norm_comm_iff

added theorem IsSubgroup.mem_trivial

added theorem IsSubgroup.mul_mem_cancel_left

added theorem IsSubgroup.mul_mem_cancel_right

added def IsSubgroup.normalizer

added theorem IsSubgroup.normalizer_isSubgroup

added theorem IsSubgroup.of_div

added theorem IsSubgroup.subset_normalizer

added def IsSubgroup.trivial

added theorem IsSubgroup.trivial_eq_closure

added theorem IsSubgroup.trivial_normal

added theorem IsSubgroup.univ_subgroup

added structure IsSubgroup

added theorem Multiplicative.isNormalSubgroup

added theorem Multiplicative.isNormalSubgroup_iff

added theorem Multiplicative.isSubgroup

added theorem Multiplicative.isSubgroup_iff

added theorem Subgroup.isSubgroup

added def Subgroup.of

added theorem Subgroup.of_normal

added theorem isNormalSubgroup_of_commGroup

added theorem isSubgroup_unionᵢ_of_directed