Basic

📁 Source: Mathlib/Algebra/Ring/Subring/Basic.lean

Statistics

Metric	Count
Definitions `ofLeftInverse`, `restrict`, `subringCongr`, `subringMap`, `eqLocus`, `fintypeRange`, `range`, `rangeRestrict`, `center`, `centerCongr`, `centerToMulOpposite`, `centralizer`, `closure`, `closureCommRingOfComm`, `comap`, `decidableMemCenter`, `equivMapOfInjective`, `gi`, `inclusion`, `instBot`, `instCommRingSubtypeMemCenter`, `instCompleteLattice`, `instDistribMulActionSubtypeMem`, `instField`, `instFintypeSubtypeMemTop`, `instInfSet`, `instInhabited`, `instMin`, `instModuleSubtypeMem`, `instMulActionSubtypeMem`, `instMulActionWithZeroSubtypeMem`, `instMulDistribMulActionSubtypeMem`, `instMulSemiringActionSubtypeMem`, `instSMulSubtypeMem`, `instSMulWithZeroSubtypeMem`, `instTop`, `map`, `prod`, `prodEquiv`, `topEquiv`	40
Theorems `int_mul_mem`, `ofLeftInverse_apply`, `ofLeftInverse_symm_apply`, `restrict_apply_coe`, `restrict_symm_apply_coe`, `closure_preimage_le`, `coe_range`, `coe_rangeRestrict`, `eqLocus_same`, `eqOn_set_closure`, `eq_of_eqOn_set_dense`, `eq_of_eqOn_set_top`, `map_closure`, `map_range`, `mem_eqLocus`, `mem_range`, `mem_range_self`, `rangeRestrict_surjective`, `range_eq_map`, `range_eq_top`, `range_eq_top_of_surjective`, `recOn`, `card_top`, `coe_div`, `coe_inv`, `smulCommClass_left`, `smulCommClass_right`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_eq_top`, `center_le_centralizer`, `center_toSubsemiring`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toSubmonoid`, `centralizer_toSubsemiring`, `centralizer_univ`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_insert_intCast`, `closure_insert_natCast`, `closure_insert_one`, `closure_insert_zero`, `closure_le`, `closure_le_centralizer_centralizer`, `closure_mono`, `closure_preimage_le`, `closure_sUnion`, `closure_singleton_intCast`, `closure_singleton_natCast`, `closure_singleton_one`, `closure_singleton_zero`, `closure_union`, `closure_univ`, `coe_bot`, `coe_center`, `coe_centralizer`, `coe_comap`, `coe_equivMapOfInjective_apply`, `coe_iInf`, `coe_iSup_of_directed`, `coe_inclusion`, `coe_inf`, `coe_map`, `coe_prod`, `coe_sInf`, `coe_sSup_of_directedOn`, `coe_top`, `comap_comap`, `comap_equiv_eq_map_symm`, `comap_iInf`, `comap_inf`, `comap_map_eq`, `comap_map_eq_self`, `comap_map_eq_self_of_injective`, `comap_top`, `eq_top_iff'`, `exists_list_of_mem_closure`, `gc_map_comap`, `instFaithfulSMulSubtypeMem`, `instIsScalarTowerSubtypeMem`, `instSMulCommClassSubtypeMemCenter`, `instSMulCommClassSubtypeMemCenter_1`, `list_prod_mem`, `list_sum_mem`, `map_bot`, `map_comap_eq`, `map_comap_eq_self`, `map_comap_eq_self_of_surjective`, `map_equiv_eq_comap_symm`, `map_iInf`, `map_iSup`, `map_id`, `map_inf`, `map_le_iff_le_comap`, `map_map`, `map_sup`, `mem_bot`, `mem_center_iff`, `mem_centralizer_iff`, `mem_closure`, `mem_closure_iff`, `mem_closure_image_of`, `mem_closure_of_mem`, `mem_comap`, `mem_iInf`, `mem_iSup_of_directed`, `mem_inf`, `mem_map`, `mem_map_equiv`, `mem_prod`, `mem_sInf`, `mem_sSup_of_directedOn`, `mem_top`, `multiset_prod_mem`, `multiset_sum_mem`, `notMem_of_notMem_closure`, `prod_bot_sup_bot_prod`, `prod_mem`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_top`, `range_fst`, `range_snd`, `range_subtype`, `sInf_toAddSubgroup`, `sInf_toSubmonoid`, `smulCommClass_left`, `smulCommClass_right`, `smul_def`, `subset_closure`, `sum_mem`, `toAddSubgroup_eq_top`, `toAddSubgroup_le_toAddSubgroup`, `toAddSubgroup_lt_toAddSubgroup`, `toAddSubgroup_mono`, `toAddSubgroup_strictMono`, `toAddSubgroup_top`, `toSubmonoid_mono`, `toSubmonoid_strictMono`, `toSubsemiring_eq_top`, `toSubsemiring_le_toSubsemiring`, `toSubsemiring_lt_toSubsemiring`, `toSubsemiring_mono`, `toSubsemiring_strictMono`, `toSubsemiring_top`, `topEquiv_apply`, `topEquiv_symm_apply_coe`, `top_prod`, `top_prod_top`	157
Total	197

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`int_mul_mem` 📖	mathematical	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SetLike.instMembership` `instSetLike`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast`	—	`zsmul_eq_mul` `zsmul_mem`

RingEquiv

Definitions

Name	Category	Theorems
`ofLeftInverse` 📖	CompOp	2 math math: `ofLeftInverse_symm_apply`, `ofLeftInverse_apply`
`restrict` 📖	CompOp	2 math math: `restrict_symm_apply_coe`, `restrict_apply_coe`
`subringCongr` 📖	CompOp	—
`subringMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLeftInverse_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Subring.toRing` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `ofLeftInverse`	—	—
`ofLeftInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`RingEquiv` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Subring.toRing` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `ofLeftInverse`	—	—
`restrict_apply_coe` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike`	`SubsemiringClass.toNonAssocSemiring` `restrict`	—	—
`restrict_symm_apply_coe` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike`	`SubsemiringClass.toNonAssocSemiring` `symm` `restrict`	—	—

RingHom

Definitions

Name	Category	Theorems
`eqLocus` 📖	CompOp	7 math math: `TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst`, `TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd`, `eqLocus_same`, `TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd`, `TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff`, `TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst`, `mem_eqLocus`
`fintypeRange` 📖	CompOp	—
`range` 📖	CompOp	72 math math: `NumberField.canonicalEmbedding.mem_span_latticeBasis`, `IsPurelyInseparable.inseparable'`, `IsPurelyInseparable.elemExponent_min'`, `rangeRestrict_surjective`, `range_eq_top_of_surjective`, `Polynomial.Splits.mem_range_of_isRoot`, `IsPurelyInseparable.elemExponent_min`, `IsPurelyInseparable.elemExponent_def'`, `IsPurelyInseparable.hasExponent_iff`, `Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one`, `RingEquiv.ofLeftInverse_symm_apply`, `RingCon.comapQuotientEquivRange_symm_mk`, `RingEquiv.ofLeftInverse_apply`, `IsPurelyInseparable.exists_pow_mem_range_tensorProduct`, `ker_rangeRestrict`, `mem_range`, `ValuationRing.range_algebraMap_eq`, `IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one`, `mem_range_self`, `mem_perfectClosure_iff_pow_mem`, `Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range`, `RingCon.comapQuotientEquivRange_mk`, `minpoly.two_le_natDegree_iff`, `IsPurelyInseparable.HasExponent.has_exponent`, `map_range`, `isPurelyInseparable_iff_pow_mem`, `isNoetherianRing_range`, `mem_perfectClosure_iff`, `IsPurelyInseparable.exponent_def'`, `mem_range_of_deriv_eq_zero`, `FractionalIdeal.mem_dual`, `minpoly.mem_range_of_degree_eq_one`, `RingCon.coe_comapQuotientEquivRange_mk`, `RingCon.kerLift_range_eq`, `IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem`, `Polynomial.filter_roots_map_range_eq_map_roots`, `Subring.map_comap_eq`, `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq`, `RingCon.range_mk'`, `isPurelyInseparable_iff`, `Polynomial.mem_map_range`, `minpoly.degree_eq_one_iff`, `IsPurelyInseparable.pow_mem`, `NumberField.mem_span_integralBasis`, `isArtinianRing_range`, `range_eq_map`, `Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable`, `minpoly.natSepDegree_eq_one_iff_pow_mem`, `Submodule.mem_traceDual`, `range_eq_top`, `IsPurelyInseparable.exponent_min`, `AlgebraicGeometry.Proj.valuativeCriterion_existence_aux`, `Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible`, `IsPurelyInseparable.hasExponent_iff'`, `RingCon.range_lift`, `IsIntegral.mem_range_algebraMap_of_minpoly_splits`, `minpoly.natDegree_eq_one_iff`, `IsPurelyInseparable.exponent_min'`, `bijective_rangeRestrict_comp_of_valuationRing`, `IsFractionRing.lift_fieldRange`, `Subring.range_subtype`, `RootPairing.toLinearMap_apply_apply_mem_range_algebraMap`, `AlgebraicGeometry.exists_lift_of_germInjective_aux`, `IsPurelyInseparable.exponent_def`, `IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar`, `Subalgebra.range_algebraMap`, `Differential.ContainConstants.mem_range_of_deriv_eq_zero`, `IsPurelyInseparable.inseparable`, `coe_range`, `coe_rangeRestrict`, `IsPurelyInseparable.elemExponent_def`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem`
`rangeRestrict` 📖	CompOp	4 math math: `rangeRestrict_surjective`, `ker_rangeRestrict`, `bijective_rangeRestrict_comp_of_valuationRing`, `coe_rangeRestrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_preimage_le` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `Subring.instPartialOrder` `Subring.closure` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike` `Subring.comap`	—	`Subring.closure_le` `SetLike.mem_coe` `Subring.mem_comap` `Subring.subset_closure`
`coe_range` 📖	mathematical	—	`SetLike.coe` `Subring` `Subring.instSetLike` `range` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	—
`coe_rangeRestrict` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subring.toRing` `instFunLike` `rangeRestrict`	—	—
`eqLocus_same` 📖	mathematical	—	`eqLocus` `Top.top` `Subring` `Subring.instTop`	—	`SetLike.ext`
`eqOn_set_closure` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	`SetLike.coe` `Subring` `Subring.instSetLike` `Subring.closure`	—	`Subring.closure_le`
`eq_of_eqOn_set_dense` 📖	—	`Subring.closure` `Top.top` `Subring` `Subring.instTop` `Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	—	`eq_of_eqOn_set_top` `eqOn_set_closure`
`eq_of_eqOn_set_top` 📖	—	`Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike` `SetLike.coe` `Subring` `Subring.instSetLike` `Top.top` `Subring.instTop`	—	—	`ext`
`map_closure` 📖	mathematical	—	`Subring.map` `Subring.closure` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	`GaloisConnection.l_comm_of_u_comm` `Set.image_preimage` `Subring.gc_map_comap` `GaloisInsertion.gc`
`map_range` 📖	mathematical	—	`Subring.map` `range` `comp` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`range_eq_map` `Subring.map_map`
`mem_eqLocus` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `eqLocus` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	—
`mem_range` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	—
`mem_range_self` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	`mem_range`
`rangeRestrict_surjective` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subring.toRing` `instFunLike` `rangeRestrict`	—	`mem_range`
`range_eq_map` 📖	mathematical	—	`range` `Subring.map` `Top.top` `Subring` `Subring.instTop`	—	`Subring.ext`
`range_eq_top` 📖	mathematical	—	`range` `Top.top` `Subring` `Subring.instTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	—	`SetLike.ext'_iff` `coe_range` `Subring.coe_top` `Set.range_eq_univ`
`range_eq_top_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	`range` `Top.top` `Subring` `Subring.instTop`	—	`range_eq_top`

Subring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	28 math math: `mem_center_iff`, `center.smulCommClass_right`, `instSMulCommClassSubtypeMemCenter`, `centralizer_eq_top_iff_subset`, `center.coe_div`, `center.coe_inv`, `centerCongr_apply_coe`, `ExpChar.expChar_center_iff`, `center_eq_top`, `CharP.charP_center_iff`, `centerToMulOpposite_symm_apply_coe`, `centralizer_univ`, `center_toSubsemiring`, `centerToMulOpposite_apply_coe`, `IsSimpleRing.isField_center`, `centerCongr_symm_apply_coe`, `center.smulCommClass_left`, `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent`, `instCharPLinearMapSubtypeMemSubringCenterId`, `instSMulCommClassSubtypeMemCenter_1`, `instExpCharLinearMapSubtypeMemSubringCenterId`, `coe_center`, `Subalgebra.center_toSubring`, `LinearMap.commute_transvections_iff_of_basis`, `Matrix.subringCenter_eq_scalar_map`, `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis`, `JacobsonNoether.exists_separable_and_not_isCentral`, `center_le_centralizer`
`centerCongr` 📖	CompOp	2 math math: `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`
`centerToMulOpposite` 📖	CompOp	2 math math: `centerToMulOpposite_symm_apply_coe`, `centerToMulOpposite_apply_coe`
`centralizer` 📖	CompOp	9 math math: `centralizer_toSubsemiring`, `centralizer_eq_top_iff_subset`, `closure_le_centralizer_centralizer`, `centralizer_le`, `centralizer_univ`, `mem_centralizer_iff`, `coe_centralizer`, `center_le_centralizer`, `centralizer_toSubmonoid`
`closure` 📖	CompOp	51 math math: `CommRingCat.closure_range_union_range_eq_top_of_isPushout`, `Polynomial.monic_restriction`, `closure_singleton_intCast`, `closure_singleton_one`, `Polynomial.eval₂_restriction`, `Algebra.mem_adjoin_iff`, `Polynomial.restriction_one`, `closure_singleton_natCast`, `Polynomial.degree_restriction`, `closure_mono`, `Subfield.mem_closure_iff`, `mem_closure`, `iInf_valuationSubring_superset`, `comap_map_eq`, `closure_union`, `closure_eq`, `closure_le_centralizer_centralizer`, `Polynomial.restriction_zero`, `closure_insert_natCast`, `is_noetherian_subring_closure`, `Algebra.adjoin_eq_ring_closure`, `mem_closure_iff`, `RingHom.eqOn_set_closure`, `subset_closure`, `smul_closure`, `Subfield.subring_closure_le`, `closure_insert_zero`, `closure_preimage_le`, `Polynomial.map_restriction`, `closure_empty`, `Polynomial.mem_closure_X_union_C`, `isIntegral_iff_isIntegral_closure_finite`, `unop_closure`, `Polynomial.coeff_restriction`, `NonUnitalSubring.unitization_range`, `closure_singleton_zero`, `mem_closure_of_mem`, `closure_insert_one`, `Polynomial.natDegree_restriction`, `op_closure`, `closure_univ`, `Polynomial.coeff_restriction'`, `Polynomial.support_restriction`, `closure_le`, `Algebra.adjoin_int`, `closure_insert_intCast`, `RingHom.closure_preimage_le`, `RingHom.map_closure`, `closure_sUnion`, `closure_iUnion`, `Algebra.TensorProduct.closure_range_union_range_eq_top`
`closureCommRingOfComm` 📖	CompOp	—
`comap` 📖	CompOp	20 math math: `coe_comap`, `top_prod`, `comap_map_eq_self`, `comap_iInf`, `comap_map_eq`, `comap_equiv_eq_map_symm`, `comap_map_eq_self_of_injective`, `closure_preimage_le`, `map_comap_eq`, `gc_map_comap`, `prod_top`, `map_equiv_eq_comap_symm`, `comap_top`, `map_comap_eq_self_of_surjective`, `mem_comap`, `map_le_iff_le_comap`, `map_comap_eq_self`, `comap_inf`, `comap_comap`, `RingHom.closure_preimage_le`
`decidableMemCenter` 📖	CompOp	—
`equivMapOfInjective` 📖	CompOp	1 math math: `coe_equivMapOfInjective_apply`
`gi` 📖	CompOp	—
`inclusion` 📖	CompOp	3 math math: `coe_inclusion`, `LocalSubring.map_maximalIdeal_eq_top_of_isMax`, `LocalSubring.le_def`
`instBot` 📖	CompOp	14 math math: `closure_singleton_intCast`, `closure_singleton_one`, `closure_singleton_natCast`, `op_bot`, `mem_bot`, `smul_bot`, `map_bot`, `prod_bot_sup_bot_prod`, `op_eq_bot`, `closure_empty`, `unop_eq_bot`, `unop_bot`, `closure_singleton_zero`, `coe_bot`
`instCommRingSubtypeMemCenter` 📖	CompOp	10 math math: `centerCongr_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `JacobsonNoether.exist_pow_eq_zero_of_le`, `centerToMulOpposite_apply_coe`, `IsSimpleRing.isField_center`, `centerCongr_symm_apply_coe`, `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent`, `LinearMap.commute_transvections_iff_of_basis`, `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis`, `JacobsonNoether.exists_separable_and_not_isCentral`
`instCompleteLattice` 📖	CompOp	18 math math: `coe_sSup_of_directedOn`, `map_iSup`, `mem_sSup_of_directedOn`, `coe_iSup_of_directed`, `op_sup`, `comap_map_eq`, `closure_union`, `op_sSup`, `prod_bot_sup_bot_prod`, `mem_iSup_of_directed`, `unop_sup`, `op_iSup`, `smul_sup`, `unop_iSup`, `unop_sSup`, `map_sup`, `closure_sUnion`, `closure_iUnion`
`instDistribMulActionSubtypeMem` 📖	CompOp	3 math math: `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent`, `LinearMap.commute_transvections_iff_of_basis`, `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis`
`instField` 📖	CompOp	4 math math: `center.coe_div`, `center.coe_inv`, `instCharPLinearMapSubtypeMemSubringCenterId`, `instExpCharLinearMapSubtypeMemSubringCenterId`
`instFintypeSubtypeMemTop` 📖	CompOp	1 math math: `card_top`
`instInfSet` 📖	CompOp	17 math math: `comap_iInf`, `iInf_valuationSubring_superset`, `LocalSubring.eq_iInf_of_isIntegrallyClosedIn`, `op_iInf`, `op_sInf`, `unop_sInf`, `Subfield.sInf_toSubring`, `sInf_toAddSubgroup`, `sInf_toSubmonoid`, `mem_iInf`, `unop_iInf`, `mem_sInf`, `eq_iInf_of_isIntegrallyClosedIn`, `Set.integer_eq`, `map_iInf`, `coe_sInf`, `coe_iInf`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	7 math math: `map_inf`, `mem_inf`, `coe_inf`, `unop_inf`, `map_comap_eq`, `op_inf`, `comap_inf`
`instModuleSubtypeMem` 📖	CompOp	8 math math: `Valuation.mem_leSubmodule_iff`, `Valuation.leSubmodule_monotone`, `Valuation.ltSubmodule_monotone`, `Valuation.ltSubmodule_le_leSubmodule`, `instCharPLinearMapSubtypeMemSubringCenterId`, `Valuation.mem_ltSubmodule_iff`, `instExpCharLinearMapSubtypeMemSubringCenterId`, `Valuation.leSubmodule_zero`
`instMulActionSubtypeMem` 📖	CompOp	—
`instMulActionWithZeroSubtypeMem` 📖	CompOp	—
`instMulDistribMulActionSubtypeMem` 📖	CompOp	—
`instMulSemiringActionSubtypeMem` 📖	CompOp	—
`instSMulSubtypeMem` 📖	CompOp	13 math math: `center.smulCommClass_right`, `instSMulCommClassSubtypeMemCenter`, `instFaithfulSMulSubtypeMem`, `smulCommClass_right`, `continuousSMul`, `center.smulCommClass_left`, `smul_def`, `LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime`, `minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure`, `instSMulCommClassSubtypeMemCenter_1`, `instIsScalarTowerSubtypeMem`, `smulCommClass_left`, `Valuation.HasExtension.instIsScalarTowerInteger`
`instSMulWithZeroSubtypeMem` 📖	CompOp	—
`instTop` 📖	CompOp	36 math math: `LocalSubring.range_toSubring`, `CommRingCat.closure_range_union_range_eq_top_of_isPushout`, `RingHom.range_eq_top_of_surjective`, `centralizer_eq_top_iff_subset`, `Algebra.toSubring_eq_top`, `top_prod`, `isLocalRing_top`, `ValuationSubring.toSubring_top`, `center_eq_top`, `eq_top_iff'`, `card_top`, `unop_top`, `toSubsemiring_top`, `topEquiv_apply`, `op_top`, `mem_top`, `top_prod_top`, `Algebra.top_toSubring`, `unop_eq_top`, `topEquiv_symm_apply_coe`, `IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring`, `coe_top`, `prod_top`, `comap_top`, `LaurentSeries.powerSeriesEquivSubring_apply`, `RingCon.range_mk'`, `RingHom.eqLocus_same`, `RingHom.range_eq_map`, `Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable`, `RingHom.range_eq_top`, `toAddSubgroup_eq_top`, `closure_univ`, `op_eq_top`, `toSubsemiring_eq_top`, `toAddSubgroup_top`, `Algebra.TensorProduct.closure_range_union_range_eq_top`
`map` 📖	CompOp	32 math math: `map_iSup`, `LocalSubring.range_toSubring`, `map_inf`, `pointwise_smul_def`, `comap_map_eq_self`, `comap_map_eq`, `comap_equiv_eq_map_symm`, `RingHom.map_range`, `map_id`, `mem_map`, `map_map`, `LocalSubring.map_toSubring`, `coe_map`, `mem_map_equiv`, `map_bot`, `comap_map_eq_self_of_injective`, `map_comap_eq`, `IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring`, `gc_map_comap`, `LaurentSeries.powerSeries_ext_subring`, `map_equiv_eq_comap_symm`, `map_comap_eq_self_of_surjective`, `LaurentSeries.powerSeriesEquivSubring_apply`, `RingHom.range_eq_map`, `instIsLocalRingSubtypeMemSubringMapOfNontrivial`, `map_le_iff_le_comap`, `map_comap_eq_self`, `coe_equivMapOfInjective_apply`, `map_iInf`, `Matrix.subringCenter_eq_scalar_map`, `map_sup`, `RingHom.map_closure`
`prod` 📖	CompOp	9 math math: `top_prod`, `mem_prod`, `prod_mono_left`, `top_prod_top`, `prod_bot_sup_bot_prod`, `prod_top`, `coe_prod`, `prod_mono`, `prod_mono_right`
`prodEquiv` 📖	CompOp	—
`topEquiv` 📖	CompOp	2 math math: `topEquiv_apply`, `topEquiv_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_top` 📖	mathematical	—	`Fintype.card` `Subring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `instFintypeSubtypeMemTop`	—	`Fintype.card_congr`
`centerCongr_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subring` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingSubtypeMemCenter` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subring` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingSubtypeMemCenter` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `centerCongr` `MulEquiv` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv`	—	—
`centerToMulOpposite_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemigroup` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subring` `instSetLike` `center` `MulOpposite.instRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingSubtypeMemCenter` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `MulOpposite` `Subring` `MulOpposite.instRing` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingSubtypeMemCenter` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_eq_top` 📖	mathematical	—	`center` `CommRing.toRing` `Top.top` `Subring` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`center_le_centralizer` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.center_subset_centralizer`
`center_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `center` `Subsemiring.center` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `Subring` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.centralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.centralizer_subset`
`centralizer_toSubmonoid` 📖	mathematical	—	`Subsemiring.toSubmonoid` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `toSubsemiring` `centralizer` `Submonoid.centralizer` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`centralizer_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `centralizer` `Subsemiring.centralizer` `Ring.toSemiring`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center`	—	`SetLike.ext'` `Set.centralizer_univ`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `Subring` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `Subring` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subring` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `Subring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ZeroMemClass.zero_mem` `Subring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass` `closure` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SubsemiringClass.toSubmonoidClass` `SetLike.instMembership`	—	—	`subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ZeroMemClass.zero_mem` `Subring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass` `closure` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SubsemiringClass.toSubmonoidClass` `SetLike.instMembership`	—	—	`subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `closure_induction`
`closure_insert_intCast` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Set.insert_eq` `closure_union` `closure_singleton_intCast` `sup_of_le_right`
`closure_insert_natCast` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Int.cast_natCast` `closure_insert_intCast`
`closure_insert_one` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Nat.cast_one` `closure_insert_natCast`
`closure_insert_zero` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Nat.cast_zero` `closure_insert_natCast`
`closure_le` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_centralizer_centralizer`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_preimage_le` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `comap`	—	`closure_le` `SetLike.mem_coe` `mem_comap` `subset_closure`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `iSup` `Subring` `Set` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `GaloisInsertion.gc`
`closure_singleton_intCast` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Bot.bot` `Subring` `instBot`	—	`bot_unique` `closure_le` `Set.singleton_subset_iff` `intCast_mem` `instSubringClass`
`closure_singleton_natCast` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Bot.bot` `Subring` `instBot`	—	`Int.cast_natCast` `closure_singleton_intCast`
`closure_singleton_one` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Bot.bot` `Subring` `instBot`	—	`Nat.cast_one` `closure_singleton_natCast`
`closure_singleton_zero` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Bot.bot` `Subring` `instBot`	—	`Nat.cast_zero` `closure_singleton_natCast`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `Subring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `Subring` `instTop`	—	`closure_eq` `coe_top`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `Bot.bot` `instBot` `Set.range` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`RingHom.coe_range`
`coe_center` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `center` `Set.center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `centralizer` `Set.centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`coe_comap` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `comap` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	—
`coe_equivMapOfInjective_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`Subring` `SetLike.instMembership` `instSetLike` `map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivMapOfInjective`	—	—
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `mem_iSup_of_directed`
`coe_inclusion` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `toRing` `RingHom.instFunLike` `inclusion`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_map` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `map` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `Subring` `Prod.instRing` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subring` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `mem_sSup_of_directedOn`
`coe_top` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	—	`comap` `RingHom.comp` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`comap_equiv_eq_map_symm` 📖	mathematical	—	`comap` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map` `RingEquiv.symm`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_equiv_eq_comap_symm`
`comap_iInf` 📖	mathematical	—	`comap` `iInf` `Subring` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_inf` 📖	mathematical	—	`comap` `Subring` `instMin`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_map_eq` 📖	mathematical	—	`comap` `map` `Subring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `closure` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`le_antisymm` `mem_map` `mem_comap` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_self` `closure_eq` `closure_union` `add_sub_cancel` `add_mem` `subset_closure` `map_le_iff_le_comap` `map_sup` `RingHom.map_closure` `le_of_eq` `sup_eq_left` `closure_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_preimage_subset` `Set.singleton_subset_iff` `zero_mem`
`comap_map_eq_self` 📖	mathematical	`Set` `Set.instHasSubset` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.coe` `Subring` `instSetLike`	`comap` `map`	—	`left_eq_sup` `closure_le` `comap_map_eq`
`comap_map_eq_self_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`comap` `map`	—	`SetLike.coe_injective` `Set.preimage_image_eq`
`comap_top` 📖	mathematical	—	`comap` `Top.top` `Subring` `instTop`	—	`GaloisConnection.u_top` `gc_map_comap`
`eq_top_iff'` 📖	mathematical	—	`Top.top` `Subring` `instTop` `SetLike.instMembership` `instSetLike`	—	`eq_top_iff` `mem_top`
`exists_list_of_mem_closure` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toMul`	—	`AddSubgroup.closure_induction` `Submonoid.exists_list_of_mem_closure` `add_zero` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `neg_zero` `neg_mul` `one_mul` `neg_add_rev` `add_comm` `mem_closure_iff`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `Subring` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`instFaithfulSMulSubtypeMem` 📖	mathematical	—	`FaithfulSMul` `Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.faithfulSMul`
`instIsScalarTowerSubtypeMem` 📖	mathematical	—	`IsScalarTower` `Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.isScalarTower`
`instSMulCommClassSubtypeMemCenter` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `instSetLike` `center` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulAction.toSemigroupAction` `instSMulSubtypeMem`	—	`Submonoid.instSMulCommClassSubtypeMemCenter_1`
`instSMulCommClassSubtypeMemCenter_1` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `instSetLike` `center` `instSMulSubtypeMem` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulAction.toSemigroupAction`	—	`Submonoid.instSMulCommClassSubtypeMemCenter`
`list_prod_mem` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`list_prod_mem` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`list_sum_mem` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`list_sum_mem` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`map_bot` 📖	mathematical	—	`map` `Bot.bot` `Subring` `instBot`	—	`GaloisConnection.l_bot` `gc_map_comap`
`map_comap_eq` 📖	mathematical	—	`map` `comap` `Subring` `instMin` `RingHom.range`	—	`SetLike.coe_injective` `Set.image_preimage_eq_inter_range`
`map_comap_eq_self` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RingHom.range`	`map` `comap`	—	`inf_of_le_left` `map_comap_eq`
`map_comap_eq_self_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`map` `comap`	—	`map_comap_eq_self` `RingHom.range_eq_top_of_surjective`
`map_equiv_eq_comap_symm` 📖	mathematical	—	`map` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `comap` `RingEquiv.symm`	—	`SetLike.coe_injective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Equiv.image_eq_preimage_symm`
`map_iInf` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`map` `iInf` `Subring` `instInfSet`	—	`SetLike.coe_injective` `coe_iInf` `Set.InjOn.image_iInter_eq` `Set.injOn_of_injective`
`map_iSup` 📖	mathematical	—	`map` `iSup` `Subring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`SetLike.coe_injective` `Set.image_id`
`map_inf` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`map` `Subring` `instMin`	—	`SetLike.coe_injective` `Set.image_inter`
`map_le_iff_le_comap` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`SetLike.coe_injective` `Set.image_image`
`map_sup` 📖	mathematical	—	`map` `Subring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`mem_bot` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`RingHom.mem_range`
`mem_center_iff` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Subsemigroup.mem_center_iff`
`mem_centralizer_iff` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`mem_closure` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `closure` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike` `AddSubgroup.closure` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Submonoid.instSetLike` `Submonoid.closure`	—	`closure_induction` `AddSubgroup.subset_closure` `Submonoid.subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `AddSubgroup.closure_induction₂` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `neg_mul` `mul_neg` `AddSubgroup.closure_induction` `Submonoid.closure_induction` `subset_closure` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `instSubringClass` `SubsemiringClass.toSubmonoidClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toNegMemClass`
`mem_closure_image_of` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike` `closure`	`Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	`RingHom.map_closure` `mem_map`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Subring` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	—
`mem_iInf` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup_of_directed` 📖	mathematical	`Directed` `Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`Submonoid.coe_iSup_of_directed` `AddSubgroup.coe_iSup_of_directed` `iSup_le` `Set.mem_iUnion` `le_iSup`
`mem_inf` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_map` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	—
`mem_map_equiv` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `map` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `DFunLike.coe` `RingEquiv.symm`	—	`Set.mem_image_equiv`
`mem_prod` 📖	mathematical	—	`Subring` `Prod.instRing` `SetLike.instMembership` `instSetLike` `prod`	—	—
`mem_sInf` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subring` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set` `Set.instMembership`	—	`sSup_eq_iSup'` `mem_iSup_of_directed` `Set.Nonempty.to_subtype` `DirectedOn.directed_val`
`mem_top` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`multiset_prod_mem` 📖	mathematical	`Subring` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`Multiset.prod` `CommRing.toCommMonoid`	—	`multiset_prod_mem` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`multiset_sum_mem` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike`	`Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`multiset_sum_mem` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`notMem_of_notMem_closure` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`prod_bot_sup_bot_prod` 📖	mathematical	—	`Subring` `Prod.instRing` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `prod` `Bot.bot` `instBot`	—	`le_antisymm` `sup_le` `prod_mono_right` `bot_le` `prod_mono_left` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass` `le_sup_left` `SetLike.mem_coe` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `le_sup_right` `Prod.fst_mul_snd`
`prod_mem` 📖	mathematical	`Subring` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`Finset.prod` `CommRing.toCommMonoid`	—	`prod_mem` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`prod_mono` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instRing` `prod`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	—	`Monotone` `Subring` `Prod.instRing` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_mono_right` 📖	mathematical	—	`Monotone` `Subring` `Prod.instRing` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_top` 📖	mathematical	—	`prod` `Top.top` `Subring` `instTop` `comap` `Prod.instRing` `RingHom.fst` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`ext`
`range_fst` 📖	mathematical	—	`RingHom.rangeS` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.fst` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	`RingHom.rangeS_top_of_surjective` `Prod.fst_surjective` `Zero.instNonempty`
`range_snd` 📖	mathematical	—	`RingHom.rangeS` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.snd` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	`RingHom.rangeS_top_of_surjective` `Prod.snd_surjective` `Zero.instNonempty`
`range_subtype` 📖	mathematical	—	`RingHom.range` `Subring` `SetLike.instMembership` `instSetLike` `toRing` `subtype`	—	`SetLike.coe_injective` `RingHom.coe_rangeS` `Subtype.range_coe`
`sInf_toAddSubgroup` 📖	mathematical	—	`toAddSubgroup` `InfSet.sInf` `Subring` `instInfSet` `iInf` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instInfSet` `Set` `Set.instMembership`	—	`mk'_toAddSubgroup`
`sInf_toSubmonoid` 📖	mathematical	—	`Subsemiring.toSubmonoid` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `toSubsemiring` `InfSet.sInf` `Subring` `instInfSet` `iInf` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instInfSet` `Set` `Set.instMembership`	—	`mk'_toSubmonoid`
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.smulCommClass_left`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.smulCommClass_right`
`smul_def` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	—
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subring` `instSetLike` `closure`	—	`mem_closure`
`sum_mem` 📖	mathematical	`Subring` `SetLike.instMembership` `instSetLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sum_mem` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `instSubringClass`
`toAddSubgroup_eq_top` 📖	mathematical	—	`toAddSubgroup` `Top.top` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instTop` `Subring` `instTop`	—	—
`toAddSubgroup_le_toAddSubgroup` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	—
`toAddSubgroup_lt_toAddSubgroup` 📖	mathematical	`Subring` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	—
`toAddSubgroup_mono` 📖	mathematical	—	`Monotone` `Subring` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `PartialOrder.toPreorder` `instPartialOrder` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	`StrictMono.monotone` `toAddSubgroup_strictMono`
`toAddSubgroup_strictMono` 📖	mathematical	—	`StrictMono` `Subring` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `PartialOrder.toPreorder` `instPartialOrder` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	—
`toAddSubgroup_top` 📖	mathematical	—	`toAddSubgroup` `Top.top` `Subring` `instTop` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instTop`	—	—
`toSubmonoid_mono` 📖	mathematical	—	`Monotone` `Subring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Submonoid.instPartialOrder` `Subsemiring.toSubmonoid` `toSubsemiring`	—	`StrictMono.monotone` `toSubmonoid_strictMono`
`toSubmonoid_strictMono` 📖	mathematical	—	`StrictMono` `Subring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Submonoid.instPartialOrder` `Subsemiring.toSubmonoid` `toSubsemiring`	—	—
`toSubsemiring_eq_top` 📖	mathematical	—	`toSubsemiring` `Top.top` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instTop` `Subring` `instTop`	—	—
`toSubsemiring_le_toSubsemiring` 📖	mathematical	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instPartialOrder` `toSubsemiring`	—	—
`toSubsemiring_lt_toSubsemiring` 📖	mathematical	`Subring` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instPartialOrder` `toSubsemiring`	—	—
`toSubsemiring_mono` 📖	mathematical	—	`Monotone` `Subring` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemiring.instPartialOrder` `toSubsemiring`	—	`StrictMono.monotone` `toSubsemiring_strictMono`
`toSubsemiring_strictMono` 📖	mathematical	—	`StrictMono` `Subring` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemiring.instPartialOrder` `toSubsemiring`	—	—
`toSubsemiring_top` 📖	mathematical	—	`toSubsemiring` `Top.top` `Subring` `instTop` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instTop`	—	—
`topEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Subring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `topEquiv` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instSetLike` `Subsemiring.instTop`	—	—
`topEquiv_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Top.top` `Subsemiring.instTop` `DFunLike.coe` `RingEquiv` `Subring` `instSetLike` `instTop` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `topEquiv`	—	—
`top_prod` 📖	mathematical	—	`prod` `Top.top` `Subring` `instTop` `comap` `Prod.instRing` `RingHom.snd` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`ext`
`top_prod_top` 📖	mathematical	—	`prod` `Top.top` `Subring` `instTop` `Prod.instRing`	—	`top_prod` `comap_top`

Subring.InClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`recOn` 📖	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd`	—	—	`add_neg_cancel` `Subring.exists_list_of_mem_closure` `neg_one_mul` `neg_mul_eq_mul_neg` `neg_neg`

Subring.center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.center` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Subring.instField`	—	—
`coe_inv` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.center` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Subring.instField` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	—
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `Subring.instSetLike` `Subring.center` `Subring.instSMulSubtypeMem` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Subsemiring.center.smulCommClass_left`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Subring` `SetLike.instMembership` `Subring.instSetLike` `Subring.center` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Subring.instSMulSubtypeMem`	—	`Subsemiring.center.smulCommClass_right`

---

← Back to Index