Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-28 22:51 2ec83dc5

View on Github →

chore(group_theory/submonoid): split into 3 files (#3058) Now

  • group_theory.submonoid.basic contains the definition, complete_lattice structure, and some basic facts about closure;
  • group_theory.submonoid.operations contains definitions of various operations on submonoids;
  • group_theory.submonoid.membership contains various facts about membership in a submonoid or the submonoid closure of a set.

Estimated changes

deleted theorem add_submonoid.smul_mem
deleted structure add_submonoid
deleted theorem monoid_hom.coe_mrange
deleted theorem monoid_hom.eq_on_mclosure
deleted theorem monoid_hom.map_mclosure
deleted theorem monoid_hom.map_mrange
deleted theorem monoid_hom.mem_mrange
deleted def monoid_hom.mrange
deleted theorem submonoid.bot_prod_bot
deleted def submonoid.closure
deleted theorem submonoid.closure_Union
deleted theorem submonoid.closure_empty
deleted theorem submonoid.closure_eq
deleted theorem submonoid.closure_le
deleted theorem submonoid.closure_mono
deleted theorem submonoid.closure_union
deleted theorem submonoid.closure_univ
deleted theorem submonoid.coe_Inf
deleted theorem submonoid.coe_bot
deleted theorem submonoid.coe_coe
deleted theorem submonoid.coe_comap
deleted theorem submonoid.coe_copy
deleted theorem submonoid.coe_eq_coe
deleted theorem submonoid.coe_inf
deleted theorem submonoid.coe_infi
deleted theorem submonoid.coe_map
deleted theorem submonoid.coe_mul
deleted theorem submonoid.coe_one
deleted theorem submonoid.coe_prod
deleted theorem submonoid.coe_ssubset_coe
deleted theorem submonoid.coe_subset_coe
deleted theorem submonoid.coe_subtype
deleted theorem submonoid.coe_top
deleted def submonoid.comap
deleted theorem submonoid.comap_comap
deleted theorem submonoid.comap_inf
deleted theorem submonoid.comap_infi
deleted theorem submonoid.comap_top
deleted def submonoid.copy
deleted theorem submonoid.copy_eq
deleted theorem submonoid.ext'
deleted theorem submonoid.ext
deleted theorem submonoid.gc_map_comap
deleted def submonoid.inclusion
deleted theorem submonoid.le_def
deleted theorem submonoid.list_prod_mem
deleted def submonoid.map
deleted theorem submonoid.map_bot
deleted theorem submonoid.map_id
deleted theorem submonoid.map_inl
deleted theorem submonoid.map_inr
deleted theorem submonoid.map_map
deleted theorem submonoid.map_sup
deleted theorem submonoid.map_supr
deleted theorem submonoid.mem_Inf
deleted theorem submonoid.mem_bot
deleted theorem submonoid.mem_carrier
deleted theorem submonoid.mem_closure
deleted theorem submonoid.mem_coe
deleted theorem submonoid.mem_comap
deleted theorem submonoid.mem_inf
deleted theorem submonoid.mem_infi
deleted theorem submonoid.mem_map
deleted theorem submonoid.mem_prod
deleted theorem submonoid.mem_sup
deleted theorem submonoid.mem_top
deleted theorem submonoid.mul_mem
deleted theorem submonoid.one_mem
deleted theorem submonoid.pow_mem
deleted def submonoid.prod
deleted theorem submonoid.prod_mem
deleted theorem submonoid.prod_mono
deleted theorem submonoid.prod_mono_left
deleted theorem submonoid.prod_mono_right
deleted theorem submonoid.prod_top
deleted theorem submonoid.range_fst
deleted theorem submonoid.range_inl'
deleted theorem submonoid.range_inl
deleted theorem submonoid.range_inr'
deleted theorem submonoid.range_inr
deleted theorem submonoid.range_snd
deleted theorem submonoid.range_subtype
deleted theorem submonoid.subset_closure
deleted def submonoid.subtype
deleted theorem submonoid.sup_eq_range
deleted theorem submonoid.top_prod
deleted theorem submonoid.top_prod_top
deleted structure submonoid
added structure add_submonoid
added theorem submonoid.closure_eq
added theorem submonoid.closure_le
added theorem submonoid.closure_mono
added theorem submonoid.closure_univ
added theorem submonoid.coe_Inf
added theorem submonoid.coe_bot
added theorem submonoid.coe_coe
added theorem submonoid.coe_copy
added theorem submonoid.coe_eq_coe
added theorem submonoid.coe_inf
added theorem submonoid.coe_infi
added theorem submonoid.coe_top
added def submonoid.copy
added theorem submonoid.copy_eq
added theorem submonoid.ext'
added theorem submonoid.ext
added theorem submonoid.le_def
added theorem submonoid.mem_Inf
added theorem submonoid.mem_bot
added theorem submonoid.mem_carrier
added theorem submonoid.mem_closure
added theorem submonoid.mem_coe
added theorem submonoid.mem_inf
added theorem submonoid.mem_infi
added theorem submonoid.mem_top
added theorem submonoid.mul_mem
added theorem submonoid.one_mem
added structure submonoid
added theorem submonoid.mem_sup
added theorem submonoid.pow_mem
added theorem submonoid.prod_mem
added theorem submonoid.sup_eq_range
added theorem monoid_hom.coe_mrange
added theorem monoid_hom.map_mrange
added theorem monoid_hom.mem_mrange
added theorem submonoid.bot_prod_bot
added theorem submonoid.coe_comap
added theorem submonoid.coe_map
added theorem submonoid.coe_mul
added theorem submonoid.coe_one
added theorem submonoid.coe_prod
added theorem submonoid.coe_subtype
added def submonoid.comap
added theorem submonoid.comap_comap
added theorem submonoid.comap_inf
added theorem submonoid.comap_infi
added theorem submonoid.comap_top
added theorem submonoid.gc_map_comap
added def submonoid.map
added theorem submonoid.map_bot
added theorem submonoid.map_id
added theorem submonoid.map_inl
added theorem submonoid.map_inr
added theorem submonoid.map_map
added theorem submonoid.map_sup
added theorem submonoid.map_supr
added theorem submonoid.mem_comap
added theorem submonoid.mem_map
added theorem submonoid.mem_prod
added theorem submonoid.mrange_fst
added theorem submonoid.mrange_inl'
added theorem submonoid.mrange_inl
added theorem submonoid.mrange_inr'
added theorem submonoid.mrange_inr
added theorem submonoid.mrange_snd
added def submonoid.prod
added theorem submonoid.prod_mono
added theorem submonoid.prod_top
added theorem submonoid.top_prod
added theorem submonoid.top_prod_top
added theorem subsemiring.nsmul_mem
deleted theorem subsemiring.smul_mem