Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-26 14:45 f4f0854c

View on Github →

feat(ring_theory/bundled_subring): add bundled subrings (#3886)

Estimated changes

Modified src/algebra/category/CommRing/limits.lean

Created src/deprecated/subring.lean

added theorem is_subring.coe_subtype

added def is_subring.subtype

added theorem is_subring_Union_of_directed

added def ring.closure

added theorem ring.closure_mono

added theorem ring.closure_subset

added theorem ring.closure_subset_iff

added theorem ring.exists_list_of_mem_closure

added theorem ring.image_closure

added theorem ring.mem_closure

added theorem ring.subset_closure

added def ring_hom.cod_restrict

Modified src/field_theory/subfield.lean

Modified src/group_theory/subgroup.lean

added def monoid_hom.cod_restrict

added theorem subgroup.coe_supr_of_directed

Modified src/linear_algebra/basic.lean

Modified src/ring_theory/algebra.lean

Modified src/ring_theory/ideal/operations.lean

Modified src/ring_theory/subring.lean

deleted theorem is_subring.coe_subtype

deleted def is_subring.subtype

deleted theorem is_subring_Union_of_directed

deleted def ring.closure

deleted theorem ring.closure_mono

deleted theorem ring.closure_subset

deleted theorem ring.closure_subset_iff

deleted theorem ring.exists_list_of_mem_closure

deleted theorem ring.image_closure

deleted theorem ring.mem_closure

deleted theorem ring.subset_closure

added def ring_equiv.subring_congr

added theorem ring_hom.closure_preimage_le

added def ring_hom.cod_restrict'

deleted def ring_hom.cod_restrict

added theorem ring_hom.coe_range

added theorem ring_hom.coe_range_restrict

added def ring_hom.eq_locus

added theorem ring_hom.eq_of_eq_on_set_dense

added theorem ring_hom.eq_of_eq_on_set_top

added theorem ring_hom.eq_on_set_closure

added theorem ring_hom.map_closure

added theorem ring_hom.map_range

added theorem ring_hom.mem_range

added def ring_hom.range

added def ring_hom.range_restrict

added theorem ring_hom.range_top_iff_surjective

added theorem ring_hom.range_top_of_surjective

added def ring_hom.restrict

added theorem ring_hom.restrict_apply

added theorem subring.Inf_to_add_subgroup

added theorem subring.Inf_to_submonoid

added theorem subring.add_mem

added def subring.closure

added theorem subring.closure_Union

added theorem subring.closure_empty

added theorem subring.closure_eq

added theorem subring.closure_eq_of_le

added theorem subring.closure_induction

added theorem subring.closure_le

added theorem subring.closure_mono

added theorem subring.closure_preimage_le

added theorem subring.closure_sUnion

added theorem subring.closure_union

added theorem subring.closure_univ

added theorem subring.coe_Inf

added theorem subring.coe_Sup_of_directed_on

added theorem subring.coe_add

added theorem subring.coe_bot

added theorem subring.coe_coe

added theorem subring.coe_comap

added theorem subring.coe_inf

added theorem subring.coe_int_mem

added theorem subring.coe_map

added theorem subring.coe_mk'

added theorem subring.coe_mul

added theorem subring.coe_neg

added theorem subring.coe_one

added theorem subring.coe_prod

added theorem subring.coe_ssubset_coe

added theorem subring.coe_subset_coe

added theorem subring.coe_subtype

added theorem subring.coe_supr_of_directed

added theorem subring.coe_to_add_subgroup

added theorem subring.coe_to_submonoid

added theorem subring.coe_top

added theorem subring.coe_zero

added def subring.comap

added theorem subring.comap_comap

added theorem subring.comap_inf

added theorem subring.comap_infi

added theorem subring.comap_top

added theorem subring.exists_list_of_mem_closure

added theorem subring.ext'

added theorem subring.ext

added theorem subring.gc_map_comap

added theorem subring.gsmul_mem

added def subring.inclusion

added theorem subring.le_def

added theorem subring.list_prod_mem

added theorem subring.list_sum_mem

added def subring.map

added theorem subring.map_bot

added theorem subring.map_le_iff_le_comap

added theorem subring.map_map

added theorem subring.map_sup

added theorem subring.map_supr

added theorem subring.mem_Inf

added theorem subring.mem_Sup_of_directed_on

added theorem subring.mem_bot

added theorem subring.mem_closure

added theorem subring.mem_closure_iff

added theorem subring.mem_coe

added theorem subring.mem_comap

added theorem subring.mem_inf

added theorem subring.mem_map

added theorem subring.mem_mk'

added theorem subring.mem_prod

added theorem subring.mem_supr_of_directed

added theorem subring.mem_to_add_subgroup

added theorem subring.mem_to_submonoid

added theorem subring.mem_top

added theorem subring.mk'_to_add_subgroup

added theorem subring.mk'_to_submonoid

added theorem subring.mul_mem

added theorem subring.multiset_prod_mem

added theorem subring.multiset_sum_mem

added theorem subring.neg_mem

added theorem subring.one_mem

added theorem subring.pow_mem

added def subring.prod

added theorem subring.prod_bot_sup_bot_prod

added def subring.prod_equiv

added theorem subring.prod_mem

added theorem subring.prod_mono

added theorem subring.prod_mono_left

added theorem subring.prod_mono_right

added theorem subring.prod_top

added theorem subring.range_fst

added theorem subring.range_snd

added theorem subring.range_subtype

added theorem subring.subset_closure

added def subring.subset_comm_ring

added def subring.subtype

added theorem subring.sum_mem

added def subring.to_comm_ring

added def subring.to_submonoid

added theorem subring.top_prod

added theorem subring.top_prod_top

added theorem subring.zero_mem

added structure subring

added def subsemiring.to_subring

Modified src/ring_theory/valuation/basic.lean