Commit 2020-05-29 06:50 b013b2d6

View on Github →

feat(ring_theory): define subsemirings (#2837) ~~Depends on #2836,~~ needs a better module docstring. Some lemmas are missing, most notably (subsemiring.closure s : set R) = add_submonoid.closure (submonoid.closure s).

Estimated changes

Modified src/group_theory/congruence.lean

Modified src/group_theory/monoid_localization.lean

Modified src/group_theory/submonoid.lean

deleted theorem monoid_hom.closure_preimage_le

added def monoid_hom.cod_mrestrict

deleted def monoid_hom.cod_restrict

added theorem monoid_hom.coe_mrange_restrict

deleted theorem monoid_hom.coe_range_restrict

added theorem monoid_hom.mclosure_preimage_le

added def monoid_hom.mrange_restrict

added def monoid_hom.mrestrict

added theorem monoid_hom.mrestrict_apply

deleted def monoid_hom.range_restrict

deleted def monoid_hom.restrict

deleted theorem monoid_hom.restrict_apply

deleted theorem monoid_hom.restrict_eq

added theorem submonoid.coe_Sup_of_directed_on

added theorem submonoid.coe_supr_of_directed

Modified src/ring_theory/localization.lean

Created src/ring_theory/subsemiring.lean

added def ring_equiv.subsemiring_congr

added def ring_hom.cod_srestrict

added theorem ring_hom.coe_srange

added theorem ring_hom.coe_srange_restrict

added theorem ring_hom.eq_of_eq_on_sdense

added theorem ring_hom.eq_of_eq_on_stop

added theorem ring_hom.eq_on_sclosure

added def ring_hom.eq_slocus

added theorem ring_hom.map_sclosure

added theorem ring_hom.map_srange

added theorem ring_hom.mem_srange

added theorem ring_hom.sclosure_preimage_le

added def ring_hom.srange

added def ring_hom.srange_restrict

added theorem ring_hom.srange_top_iff_surjective

added theorem ring_hom.srange_top_of_surjective

added def ring_hom.srestrict

added theorem ring_hom.srestrict_apply

added theorem subsemiring.Inf_to_add_submonoid

added theorem subsemiring.Inf_to_submonoid

added theorem subsemiring.add_mem

added def subsemiring.closure

added theorem subsemiring.closure_Union

added theorem subsemiring.closure_empty

added theorem subsemiring.closure_eq

added theorem subsemiring.closure_eq_of_le

added theorem subsemiring.closure_induction

added theorem subsemiring.closure_le

added theorem subsemiring.closure_mono

added theorem subsemiring.closure_sUnion

added theorem subsemiring.closure_union

added theorem subsemiring.closure_univ

added theorem subsemiring.coe_Inf

added theorem subsemiring.coe_Sup_of_directed_on

added theorem subsemiring.coe_bot

added theorem subsemiring.coe_coe

added theorem subsemiring.coe_comap

added theorem subsemiring.coe_inf

added theorem subsemiring.coe_map

added theorem subsemiring.coe_mk'

added theorem subsemiring.coe_mul

added theorem subsemiring.coe_nat_mem

added theorem subsemiring.coe_one

added theorem subsemiring.coe_prod

added theorem subsemiring.coe_ssubset_coe

added theorem subsemiring.coe_subset_coe

added theorem subsemiring.coe_subtype

added theorem subsemiring.coe_supr_of_directed

added theorem subsemiring.coe_to_add_submonoid

added theorem subsemiring.coe_to_submonoid

added theorem subsemiring.coe_top

added def subsemiring.comap

added theorem subsemiring.comap_comap

added theorem subsemiring.comap_inf

added theorem subsemiring.comap_infi

added theorem subsemiring.comap_top

added theorem subsemiring.ext'

added theorem subsemiring.ext

added theorem subsemiring.gc_map_comap

added def subsemiring.inclusion

added theorem subsemiring.le_def

added theorem subsemiring.list_prod_mem

added theorem subsemiring.list_sum_mem

added def subsemiring.map

added theorem subsemiring.map_bot

added theorem subsemiring.map_le_iff_le_comap

added theorem subsemiring.map_map

added theorem subsemiring.map_sup

added theorem subsemiring.map_supr

added theorem subsemiring.mem_Inf

added theorem subsemiring.mem_Sup_of_directed_on

added theorem subsemiring.mem_bot

added theorem subsemiring.mem_closure

added theorem subsemiring.mem_coe

added theorem subsemiring.mem_comap

added theorem subsemiring.mem_inf

added theorem subsemiring.mem_map

added theorem subsemiring.mem_mk'

added theorem subsemiring.mem_prod

added theorem subsemiring.mem_supr_of_directed

added theorem subsemiring.mem_to_add_submonoid

added theorem subsemiring.mem_to_submonoid

added theorem subsemiring.mem_top

added theorem subsemiring.mk'_to_add_submonoid

added theorem subsemiring.mk'_to_submonoid

added theorem subsemiring.mul_mem

added theorem subsemiring.multiset_prod_mem

added theorem subsemiring.multiset_sum_mem

added theorem subsemiring.one_mem

added theorem subsemiring.pow_mem

added def subsemiring.prod

added theorem subsemiring.prod_bot_sup_bot_prod

added def subsemiring.prod_equiv

added theorem subsemiring.prod_mem

added theorem subsemiring.prod_mono

added theorem subsemiring.prod_mono_left

added theorem subsemiring.prod_mono_right

added theorem subsemiring.prod_top

added theorem subsemiring.range_fst

added theorem subsemiring.range_snd

added theorem subsemiring.smul_mem

added theorem subsemiring.srange_subtype

added theorem subsemiring.subset_closure

added def subsemiring.subtype

added theorem subsemiring.sum_mem

added theorem subsemiring.top_prod

added theorem subsemiring.top_prod_top

added theorem subsemiring.zero_mem

added structure subsemiring