Commit 2023-02-11 16:08 a90dbbe1

View on Github →

feat: port RingTheory.Subring.Basic (#1945)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Subring/Basic.lean

added theorem AddSubgroup.int_mul_mem

added def RingEquiv.ofLeftInverse

added theorem RingEquiv.ofLeftInverse_apply

added theorem RingEquiv.ofLeftInverse_symm_apply

added def RingEquiv.subringCongr

added def RingEquiv.subringMap

added theorem RingHom.closure_preimage_le

added theorem RingHom.coe_range

added theorem RingHom.coe_rangeRestrict

added def RingHom.eqLocus

added theorem RingHom.eqLocus_same

added theorem RingHom.eqOn_set_closure

added theorem RingHom.eq_of_eqOn_set_dense

added theorem RingHom.eq_of_eqOn_set_top

added theorem RingHom.map_closure

added theorem RingHom.map_range

added theorem RingHom.mem_range

added theorem RingHom.mem_range_self

added def RingHom.range

added def RingHom.rangeRestrict

added theorem RingHom.rangeRestrict_surjective

added theorem RingHom.range_eq_map

added theorem RingHom.range_top_iff_surjective

added theorem RingHom.range_top_of_surjective

added theorem Subring.center.coe_div

added theorem Subring.center.coe_inv

added def Subring.center

added theorem Subring.center_eq_top

added theorem Subring.center_toSubsemiring

added def Subring.closure

added def Subring.closureCommRingOfComm

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_induction₂

added theorem Subring.closure_le

added theorem Subring.closure_mono

added theorem Subring.closure_preimage_le

added theorem Subring.closure_union

added theorem Subring.closure_unionᵢ

added theorem Subring.closure_unionₛ

added theorem Subring.closure_univ

added theorem Subring.coeSubtype

added theorem Subring.coe_add

added theorem Subring.coe_bot

added theorem Subring.coe_center

added theorem Subring.coe_comap

added theorem Subring.coe_copy

added theorem Subring.coe_eq_zero_iff

added theorem Subring.coe_equivMapOfInjective_apply

added theorem Subring.coe_inf

added theorem Subring.coe_infᵢ

added theorem Subring.coe_infₛ

added theorem Subring.coe_int_cast

added theorem Subring.coe_map

added theorem Subring.coe_mk'

added theorem Subring.coe_mul

added theorem Subring.coe_nat_cast

added theorem Subring.coe_neg

added theorem Subring.coe_one

added theorem Subring.coe_pow

added theorem Subring.coe_prod

added theorem Subring.coe_set_mk

added theorem Subring.coe_supᵢ_of_directed

added theorem Subring.coe_supₛ_of_directedOn

added theorem Subring.coe_toAddSubgroup

added theorem Subring.coe_toSubmonoid

added theorem Subring.coe_toSubsemiring

added theorem Subring.coe_top

added theorem Subring.coe_zero

added def Subring.comap

added theorem Subring.comap_comap

added theorem Subring.comap_equiv_eq_map_symm

added theorem Subring.comap_inf

added theorem Subring.comap_infᵢ

added theorem Subring.comap_top

added theorem Subring.copy_eq

added theorem Subring.eq_top_iff'

added theorem Subring.exists_list_of_mem_closure

added theorem Subring.ext

added theorem Subring.gc_map_comap

added def Subring.inclusion

added theorem Subring.infₛ_toAddSubgroup

added theorem Subring.infₛ_toSubmonoid

added def Subring.map

added theorem Subring.map_bot

added theorem Subring.map_equiv_eq_comap_symm

added theorem Subring.map_id

added theorem Subring.map_le_iff_le_comap

added theorem Subring.map_map

added theorem Subring.map_sup

added theorem Subring.map_supᵢ

added theorem Subring.mem_bot

added theorem Subring.mem_carrier

added theorem Subring.mem_center_iff

added theorem Subring.mem_closure

added theorem Subring.mem_closure_iff

added theorem Subring.mem_comap

added theorem Subring.mem_inf

added theorem Subring.mem_infᵢ

added theorem Subring.mem_infₛ

added theorem Subring.mem_map

added theorem Subring.mem_map_equiv

added theorem Subring.mem_mk'

added theorem Subring.mem_mk

added theorem Subring.mem_prod

added theorem Subring.mem_supᵢ_of_directed

added theorem Subring.mem_supₛ_of_directedOn

added theorem Subring.mem_toAddSubgroup

added theorem Subring.mem_toSubmonoid

added theorem Subring.mem_toSubsemiring

added theorem Subring.mem_top

added theorem Subring.mk'_toAddSubgroup

added theorem Subring.mk'_toSubmonoid

added theorem Subring.mk_le_mk

added theorem Subring.not_mem_of_not_mem_closure

added def Subring.prod

added def Subring.prodEquiv

added theorem Subring.prod_bot_sup_bot_prod

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.smul_def

added theorem Subring.subset_closure

added def Subring.subtype

added theorem Subring.toAddSubgroup_injective

added theorem Subring.toAddSubgroup_mono

added theorem Subring.toAddSubgroup_strictMono

added theorem Subring.toSubmonoid_injective

added theorem Subring.toSubmonoid_mono

added theorem Subring.toSubmonoid_strictMono

added theorem Subring.toSubsemiring_injective

added theorem Subring.toSubsemiring_mono

added theorem Subring.toSubsemiring_strictMono

added def Subring.topEquiv

added theorem Subring.top_prod

added theorem Subring.top_prod_top

added structure Subring

added theorem SubringClass.coeSubtype

added theorem SubringClass.coe_intCast

added theorem SubringClass.coe_natCast

added def SubringClass.subtype

added def Subsemiring.toSubring

added theorem Units.mem_posSubgroup

added def Units.posSubgroup

added theorem coe_int_mem

Modified Mathlib/RingTheory/Subsemiring/Basic.lean