Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-01 23:39 b95f1655

View on Github →

chore(group_theory/sub*): move unbundled submonoids and subgroups to deprecated (#2912)

  • move unbundled submonoids to deprecated/submonoid.lean;
  • move unbundled subgroups to deprecated/subgroup.lean;
  • move bundled subgroups to group_theory/subgroup.lean;
  • unbundled versions import bundled.

Estimated changes

added inductive add_group.in_closure
added def gmultiples
added theorem gmultiples_subset
added def gpowers
added theorem gpowers_subset
added def group.closure
added theorem group.closure_mono
added theorem group.closure_subgroup
added theorem group.closure_subset
added def group.conjugates
added theorem group.image_closure
added inductive group.in_closure
added theorem group.mclosure_subset
added theorem group.mem_closure
added theorem group.subset_closure
added theorem injective_mul
added theorem is_add_subgroup.of_sub
added def is_group_hom.ker
added theorem is_group_hom.mem_ker
added theorem is_subgroup.coe_gpow
added theorem is_subgroup.coe_inv
added theorem is_subgroup.gpow_mem
added theorem is_subgroup.mem_center
added theorem is_subgroup.of_div
added theorem mem_gmultiples
added theorem mem_gpowers
added def subgroup.of
added inductive add_monoid.in_closure
added theorem image.is_submonoid
added theorem is_submonoid.coe_mul
added theorem is_submonoid.coe_one
added theorem is_submonoid.coe_pow
added theorem is_submonoid.pow_mem
added def monoid.closure
added theorem monoid.closure_mono
added theorem monoid.closure_subset
added theorem monoid.image_closure
added inductive monoid.in_closure
added theorem monoid.subset_closure
added theorem multiples.add_mem
added theorem multiples.self_mem
added theorem multiples.zero_mem
added def multiples
added theorem powers.mul_mem
added theorem powers.one_mem
added theorem powers.self_mem
added def powers
added def submonoid.of
deleted theorem add_subgroup.gsmul_mem
deleted structure add_subgroup
deleted theorem monoid_hom.coe_range
deleted theorem monoid_hom.comap_ker
deleted def monoid_hom.eq_locus
deleted theorem monoid_hom.eq_on_closure
deleted def monoid_hom.ker
deleted theorem monoid_hom.map_closure
deleted theorem monoid_hom.map_range
deleted theorem monoid_hom.mem_ker
deleted theorem monoid_hom.mem_range
deleted def monoid_hom.range
deleted theorem subgroup.bot_prod_bot
deleted def subgroup.closure
deleted theorem subgroup.closure_Union
deleted theorem subgroup.closure_empty
deleted theorem subgroup.closure_eq
deleted theorem subgroup.closure_eq_of_le
deleted theorem subgroup.closure_le
deleted theorem subgroup.closure_mono
deleted theorem subgroup.closure_union
deleted theorem subgroup.closure_univ
deleted theorem subgroup.coe_Inf
deleted theorem subgroup.coe_bot
deleted theorem subgroup.coe_coe
deleted theorem subgroup.coe_comap
deleted theorem subgroup.coe_inf
deleted theorem subgroup.coe_inv
deleted theorem subgroup.coe_map
deleted theorem subgroup.coe_mul
deleted theorem subgroup.coe_one
deleted theorem subgroup.coe_prod
deleted theorem subgroup.coe_subset_coe
deleted theorem subgroup.coe_subtype
deleted theorem subgroup.coe_to_submonoid
deleted theorem subgroup.coe_top
deleted def subgroup.comap
deleted theorem subgroup.comap_comap
deleted theorem subgroup.comap_inf
deleted theorem subgroup.comap_infi
deleted theorem subgroup.comap_top
deleted theorem subgroup.ext'
deleted theorem subgroup.ext
deleted theorem subgroup.gc_map_comap
deleted theorem subgroup.gpow_mem
deleted theorem subgroup.inv_mem
deleted theorem subgroup.le_def
deleted theorem subgroup.list_prod_mem
deleted def subgroup.map
deleted theorem subgroup.map_bot
deleted theorem subgroup.map_map
deleted theorem subgroup.map_sup
deleted theorem subgroup.map_supr
deleted theorem subgroup.mem_Inf
deleted theorem subgroup.mem_bot
deleted theorem subgroup.mem_closure
deleted theorem subgroup.mem_coe
deleted theorem subgroup.mem_comap
deleted theorem subgroup.mem_inf
deleted theorem subgroup.mem_map
deleted theorem subgroup.mem_prod
deleted theorem subgroup.mem_top
deleted theorem subgroup.mul_mem
deleted def subgroup.of
deleted theorem subgroup.one_mem
deleted theorem subgroup.pow_mem
deleted def subgroup.prod
deleted def subgroup.prod_equiv
deleted theorem subgroup.prod_mem
deleted theorem subgroup.prod_mono
deleted theorem subgroup.prod_mono_left
deleted theorem subgroup.prod_mono_right
deleted theorem subgroup.prod_top
deleted theorem subgroup.subset_closure
deleted def subgroup.subtype
deleted theorem subgroup.top_prod
deleted theorem subgroup.top_prod_top
deleted structure subgroup
deleted inductive add_group.in_closure
added theorem add_subgroup.gsmul_mem
added structure add_subgroup
deleted theorem additive.is_add_subgroup
deleted def gmultiples
deleted theorem gmultiples_subset
deleted def gpowers
deleted theorem gpowers_subset
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 def group.conjugates
deleted theorem group.conjugates_subset
deleted theorem group.gpowers_eq_closure
deleted theorem group.image_closure
deleted inductive group.in_closure
deleted theorem group.mclosure_inv_subset
deleted theorem group.mclosure_subset
deleted theorem group.mem_closure
deleted theorem group.mem_conjugates_self
deleted theorem group.normal_closure_mono
deleted theorem group.subset_closure
deleted theorem injective_mul
deleted theorem is_add_subgroup.gsmul_coe
deleted theorem is_add_subgroup.gsmul_mem
deleted theorem is_add_subgroup.of_sub
deleted theorem is_add_subgroup.sub_mem
deleted theorem is_group_hom.inv_iff_ker'
deleted theorem is_group_hom.inv_iff_ker
deleted theorem is_group_hom.inv_ker_one'
deleted theorem is_group_hom.inv_ker_one
deleted def is_group_hom.ker
deleted theorem is_group_hom.mem_ker
deleted theorem is_group_hom.one_ker_inv'
deleted theorem is_group_hom.one_ker_inv
deleted def is_subgroup.center
deleted theorem is_subgroup.coe_gpow
deleted theorem is_subgroup.coe_inv
deleted theorem is_subgroup.gpow_mem
deleted theorem is_subgroup.inv_mem_iff
deleted theorem is_subgroup.mem_center
deleted theorem is_subgroup.mem_norm_comm
deleted theorem is_subgroup.mem_trivial
deleted theorem is_subgroup.of_div
deleted def is_subgroup.trivial
deleted theorem mem_gmultiples
deleted theorem mem_gpowers
added theorem monoid_hom.coe_range
added theorem monoid_hom.comap_ker
added def monoid_hom.ker
added theorem monoid_hom.map_closure
added theorem monoid_hom.map_range
added theorem monoid_hom.mem_ker
added theorem monoid_hom.mem_range
added def monoid_hom.range
added theorem subgroup.bot_prod_bot
added def subgroup.closure
added theorem subgroup.closure_Union
added theorem subgroup.closure_empty
added theorem subgroup.closure_eq
added theorem subgroup.closure_le
added theorem subgroup.closure_mono
added theorem subgroup.closure_union
added theorem subgroup.closure_univ
added theorem subgroup.coe_Inf
added theorem subgroup.coe_bot
added theorem subgroup.coe_coe
added theorem subgroup.coe_comap
added theorem subgroup.coe_inf
added theorem subgroup.coe_inv
added theorem subgroup.coe_map
added theorem subgroup.coe_mul
added theorem subgroup.coe_one
added theorem subgroup.coe_prod
added theorem subgroup.coe_subtype
added theorem subgroup.coe_top
added def subgroup.comap
added theorem subgroup.comap_comap
added theorem subgroup.comap_inf
added theorem subgroup.comap_infi
added theorem subgroup.comap_top
added theorem subgroup.ext'
added theorem subgroup.ext
added theorem subgroup.gc_map_comap
added theorem subgroup.gpow_mem
added theorem subgroup.inv_mem
added theorem subgroup.le_def
added theorem subgroup.list_prod_mem
added def subgroup.map
added theorem subgroup.map_bot
added theorem subgroup.map_map
added theorem subgroup.map_sup
added theorem subgroup.map_supr
added theorem subgroup.mem_Inf
added theorem subgroup.mem_bot
added theorem subgroup.mem_closure
added theorem subgroup.mem_coe
added theorem subgroup.mem_comap
added theorem subgroup.mem_inf
added theorem subgroup.mem_map
added theorem subgroup.mem_prod
added theorem subgroup.mem_top
added theorem subgroup.mul_mem
added theorem subgroup.one_mem
added theorem subgroup.pow_mem
added def subgroup.prod
added theorem subgroup.prod_mem
added theorem subgroup.prod_mono
added theorem subgroup.prod_top
added def subgroup.subtype
added theorem subgroup.top_prod
added theorem subgroup.top_prod_top
added structure subgroup
deleted inductive add_monoid.in_closure
deleted theorem additive.is_add_submonoid
deleted theorem image.is_submonoid
deleted theorem is_add_submonoid.smul_coe
deleted theorem is_add_submonoid.smul_mem
deleted theorem is_submonoid.coe_mul
deleted theorem is_submonoid.coe_one
deleted theorem is_submonoid.coe_pow
deleted theorem is_submonoid.pow_mem
deleted theorem is_submonoid.power_subset
deleted def monoid.closure
deleted theorem monoid.closure_mono
deleted theorem monoid.closure_singleton
deleted theorem monoid.closure_subset
deleted theorem monoid.image_closure
deleted inductive monoid.in_closure
deleted theorem monoid.subset_closure
deleted theorem multiples.add_mem
deleted theorem multiples.self_mem
deleted theorem multiples.zero_mem
deleted def multiples
deleted theorem powers.mul_mem
deleted theorem powers.one_mem
deleted theorem powers.self_mem
deleted def powers
deleted def submonoid.of