Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-14 00:07 9a911258

View on Github →

chore(group_theory/sub*) : rename type vars (#1982) Use M, G, A instead of greek letters

Estimated changes

Modified src/group_theory/subgroup.lean

modified inductive add_group.in_closure

modified theorem additive.normal_add_subgroup_iff

modified theorem additive.simple_add_group_iff

modified def gmultiples

modified theorem gmultiples_subset

modified def gpowers

modified theorem gpowers_subset

modified def group.closure

modified theorem group.closure_eq_mclosure

modified theorem group.closure_mono

modified theorem group.closure_subgroup

modified theorem group.closure_subset

modified theorem group.closure_subset_iff

modified theorem group.conj_mem_conjugates_of_set

modified def group.conjugates

modified def group.conjugates_of_set

modified theorem group.conjugates_of_set_mono

modified theorem group.conjugates_of_set_subset

modified theorem group.conjugates_subset

modified theorem group.exists_list_of_mem_closure

modified theorem group.gpowers_eq_closure

modified theorem group.image_closure

modified inductive group.in_closure

modified theorem group.mclosure_inv_subset

modified theorem group.mclosure_subset

modified theorem group.mem_closure

modified theorem group.mem_closure_union_iff

modified theorem group.mem_conjugates_of_set_iff

modified theorem group.mem_conjugates_self

modified def group.normal_closure

modified theorem group.normal_closure_mono

modified theorem group.normal_closure_subset

modified theorem group.normal_closure_subset_iff

modified theorem group.subset_closure

modified theorem injective_mul

modified theorem is_add_subgroup.gsmul_coe

modified theorem is_add_subgroup.gsmul_mem

modified theorem is_add_subgroup.of_sub

modified theorem is_add_subgroup.sub_mem

modified theorem is_group_hom.inj_iff_trivial_ker

modified theorem is_group_hom.inj_of_trivial_ker

modified theorem is_group_hom.inv_iff_ker'

modified theorem is_group_hom.inv_iff_ker

modified theorem is_group_hom.inv_ker_one'

modified theorem is_group_hom.inv_ker_one

modified def is_group_hom.ker

modified theorem is_group_hom.mem_ker

modified theorem is_group_hom.one_iff_ker_inv'

modified theorem is_group_hom.one_iff_ker_inv

modified theorem is_group_hom.one_ker_inv'

modified theorem is_group_hom.one_ker_inv

modified theorem is_group_hom.trivial_ker_iff_eq_one

modified theorem is_group_hom.trivial_ker_of_inj

modified def is_subgroup.center

modified theorem is_subgroup.coe_gpow

modified theorem is_subgroup.coe_inv

modified theorem is_subgroup.eq_trivial_iff

modified theorem is_subgroup.gpow_mem

modified theorem is_subgroup.mem_center

modified theorem is_subgroup.mem_norm_comm

modified theorem is_subgroup.mem_norm_comm_iff

modified theorem is_subgroup.mem_trivial

modified def is_subgroup.normalizer

modified theorem is_subgroup.of_div

modified theorem is_subgroup.subset_normalizer

modified def is_subgroup.trivial

modified theorem is_subgroup.trivial_eq_closure

modified theorem mem_gmultiples

modified theorem mem_gpowers

modified theorem multiplicative.normal_subgroup_iff

modified theorem multiplicative.simple_group_iff

modified theorem normal_subgroup_of_comm_group

deleted theorem simple_add_group_of_surjective

modified theorem simple_group_of_surjective

Modified src/group_theory/submonoid.lean

modified theorem add_monoid.closure'_singleton

modified inductive add_monoid.in_closure

modified theorem add_submonoid.coe_smul

modified theorem add_submonoid.multiples.self_mem

modified def add_submonoid.multiples

modified theorem add_submonoid.multiples_subset

modified def add_submonoid.of_submonoid

modified theorem add_submonoid.smul_mem

modified def add_submonoid.to_submonoid

modified structure add_submonoid

modified theorem image.is_submonoid

modified theorem is_add_submonoid.multiple_subset

modified theorem is_add_submonoid.smul_coe

modified theorem is_add_submonoid.smul_mem

modified theorem is_submonoid.coe_mul

modified theorem is_submonoid.coe_one

modified theorem is_submonoid.finset_prod_mem

modified theorem is_submonoid.list_prod_mem

modified theorem is_submonoid.multiset_prod_mem

modified theorem is_submonoid.pow_mem

modified theorem is_submonoid.power_subset

modified def monoid.closure

modified theorem monoid.closure_mono

modified theorem monoid.closure_singleton

modified theorem monoid.closure_subset

modified theorem monoid.exists_list_of_mem_closure

modified theorem monoid.image_closure

modified inductive monoid.in_closure

modified theorem monoid.mem_closure_union_iff

modified theorem monoid.subset_closure

modified theorem multiples.add_mem

modified theorem multiples.self_mem

modified theorem multiples.zero_mem

modified def multiples

modified theorem powers.mul_mem

modified theorem powers.one_mem

modified theorem powers.self_mem

modified def powers

modified def submonoid.add_submonoid_equiv

modified def submonoid.of_add_submonoid

modified def submonoid.to_add_submonoid

modified structure submonoid