Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-01 06:47 c7fb84ba

View on Github →

refactor(group_theory/submonoid): review API (#2173) The old API was mirroring the API for unbundled submonoids, while the new one is based on the API of submodule. Also move some facts about monoid/group structure on M × N to algebra/group/prod.

Estimated changes

added theorem free_monoid.comp_lift
added theorem free_monoid.lift_apply
added theorem monoid_hom.comp_id
added theorem monoid_hom.id_comp
added theorem monoid_hom.coe_fst
added theorem monoid_hom.coe_snd
added theorem monoid_hom.comp_coprod
added def monoid_hom.fst
added def monoid_hom.inl
added theorem monoid_hom.inl_apply
added def monoid_hom.inr
added theorem monoid_hom.inr_apply
added theorem monoid_hom.prod_apply
added theorem monoid_hom.prod_unique
added def monoid_hom.snd
added theorem prod.fst_inv
added theorem prod.fst_mul
added theorem prod.fst_mul_snd
added theorem prod.fst_one
added theorem prod.fst_sub
added theorem prod.inv_mk
added theorem prod.mk_mul_mk
added theorem prod.mk_sub_mk
added theorem prod.one_eq_mk
added theorem prod.snd_inv
added theorem prod.snd_mul
added theorem prod.snd_one
added theorem prod.snd_sub
deleted theorem prod.fst_inv
deleted theorem prod.fst_mul
deleted theorem prod.fst_one
deleted theorem prod.fst_sub
deleted theorem prod.inv_mk
deleted theorem prod.mk_mul_mk
deleted theorem prod.mk_sub_mk
deleted def prod.monoid_hom.fst
deleted def prod.monoid_hom.inl
deleted def prod.monoid_hom.inr
deleted def prod.monoid_hom.snd
deleted theorem prod.one_eq_mk
deleted theorem prod.snd_inv
deleted theorem prod.snd_mul
deleted theorem prod.snd_one
deleted theorem prod.snd_sub
deleted def submonoid.prod
added theorem prod.fst_injective
added theorem prod.fst_surjective
added theorem prod.snd_injective
added theorem prod.snd_surjective
modified theorem con.ker_lift_range_eq
modified theorem con.lift_range
deleted theorem add_submonoid.coe_smul
modified theorem add_submonoid.smul_mem
deleted def monoid.closure'
deleted theorem monoid.closure'_le
deleted theorem monoid.closure'_mono
deleted theorem monoid.closure'_singleton
deleted theorem monoid.image_closure'
deleted theorem monoid.le_closure'
added theorem monoid_hom.coe_mrange
deleted def monoid_hom.comap
deleted def monoid_hom.map
added theorem monoid_hom.map_mrange
added theorem monoid_hom.mem_mrange
deleted def monoid_hom.range
deleted def monoid_hom.range_mk
modified def monoid_hom.restrict
deleted theorem submonoid.Inf_le'
deleted def submonoid.bot
added theorem submonoid.bot_prod_bot
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_comap
added theorem submonoid.coe_inf
added theorem submonoid.coe_map
deleted theorem submonoid.coe_pow
added theorem submonoid.coe_prod
added theorem submonoid.coe_subtype
added theorem submonoid.coe_top
added def submonoid.comap
added theorem submonoid.comap_comap
added theorem submonoid.comap_inf
added theorem submonoid.comap_infi
added theorem submonoid.comap_top
deleted theorem submonoid.finset_prod_mem
added theorem submonoid.gc_map_comap
deleted def submonoid.inf
deleted theorem submonoid.le_Inf'
modified theorem submonoid.le_def
modified theorem submonoid.list_prod_mem
added def submonoid.map
added theorem submonoid.map_bot
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_closure
modified theorem submonoid.mem_coe
added theorem submonoid.mem_comap
modified theorem submonoid.mem_inf
added theorem submonoid.mem_map
added theorem submonoid.mem_prod
added theorem submonoid.mem_sup
added def submonoid.of
modified theorem submonoid.pow_mem
deleted theorem submonoid.powers.self_mem
deleted def submonoid.powers
deleted theorem submonoid.powers_subset
added def submonoid.prod
added theorem submonoid.prod_mono
added theorem submonoid.prod_top
added theorem submonoid.range_fst
added theorem submonoid.range_inl'
added theorem submonoid.range_inl
added theorem submonoid.range_inr'
added theorem submonoid.range_inr
added theorem submonoid.range_snd
modified def submonoid.subtype
deleted theorem submonoid.subtype_apply
deleted theorem submonoid.subtype_eq_val
added theorem submonoid.sup_eq_range
added theorem submonoid.top_prod
added theorem submonoid.top_prod_top
deleted def submonoid.univ