Basic

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

Statistics

Metric	Count
Definitions `ofLeftInverseS`, `subsemiringCongr`, `subsemiringMap`, `codRestrict`, `fintypeRangeS`, `rangeS`, `rangeSRestrict`, `restrict`, `subsemiringClosure`, `center`, `commSemiring`, `commSemiring'`, `centerCongr`, `centerToMulOpposite`, `centralizer`, `closure`, `closureCommSemiringOfComm`, `comap`, `decidableMemCenter`, `distribMulAction`, `equivMapOfInjective`, `gi`, `inclusion`, `instBot`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instModuleSubtypeMem`, `instMulActionWithZeroSubtypeMem`, `instMulSemiringActionSubtypeMem`, `instSMulWithZeroSubtypeMem`, `instSMulWithZeroSubtypeMem_1`, `map`, `mulAction`, `mulActionWithZero`, `mulDistribMulAction`, `prod`, `prodEquiv`, `smul`, `topEquiv`	40
Theorems `ofLeftInverseS_apply`, `ofLeftInverseS_symm_apply`, `subsemiringMap_apply_coe`, `subsemiringMap_symm_apply_coe`, `codRestrict_apply`, `coe_rangeS`, `coe_rangeSRestrict`, `coe_restrict_apply`, `comp_restrict`, `eqOn_sclosure`, `eq_of_eqOn_sdense`, `eq_of_eqOn_stop`, `injective_codRestrict`, `map_closureS`, `map_rangeS`, `mem_rangeS`, `mem_rangeS_self`, `rangeSRestrict_surjective`, `rangeS_codRestrict`, `rangeS_eq_map`, `rangeS_eq_top`, `rangeS_toSubmonoid`, `rangeS_top_iff_surjective`, `rangeS_top_of_surjective`, `sclosure_preimage_le`, `surjective_codRestrict`, `subsemiringClosure_coe`, `subsemiringClosure_eq_closure`, `subsemiringClosure_mem`, `subsemiringClosure_toAddSubmonoid`, `subsemiringClosure_toNonUnitalSubsemiring`, `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_toSubmonoid`, `centralizer_centralizer_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toSubmonoid`, `centralizer_univ`, `closure_addSubmonoid_closure`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_insert_natCast`, `closure_insert_one`, `closure_insert_zero`, `closure_le`, `closure_le_centralizer_centralizer`, `closure_mono`, `closure_sUnion`, `closure_singleton_natCast`, `closure_singleton_one`, `closure_singleton_zero`, `closure_submonoid_closure`, `closure_union`, `closure_univ`, `coe_bot`, `coe_center`, `coe_centralizer`, `coe_closure_eq`, `coe_comap`, `coe_equivMapOfInjective_apply`, `coe_iInf`, `coe_iSup_of_directed`, `coe_map`, `coe_prod`, `coe_sInf`, `coe_sSup_of_directedOn`, `comap_comap`, `comap_equiv_eq_map_symm`, `comap_iInf`, `comap_inf`, `comap_map_eq_self_of_injective`, `comap_toSubmonoid`, `comap_top`, `eq_top_iff'`, `faithfulSMul`, `gc_map_comap`, `inclusion_injective`, `instFaithfulSMulSubtypeMem`, `instSMulCommClassSubtypeMemCenter`, `instSMulCommClassSubtypeMemCenter_1`, `isScalarTower`, `le_centralizer_centralizer`, `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`, `map_toSubmonoid`, `mem_bot`, `mem_center_iff`, `mem_centralizer_iff`, `mem_closure`, `mem_closure_iff`, `mem_closure_iff_exists_list`, `mem_closure_of_mem`, `mem_comap`, `mem_iInf`, `mem_iSup_of_directed`, `mem_map`, `mem_map_equiv`, `mem_prod`, `mem_sInf`, `mem_sSup_of_directedOn`, `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`, `rangeS_subtype`, `range_fst`, `range_snd`, `sInf_toAddSubmonoid`, `sInf_toSubmonoid`, `smulCommClass_left`, `smulCommClass_right`, `smul_def`, `subset_closure`, `sum_mem`, `toAddSubmonoid_mono`, `toAddSubmonoid_strictMono`, `toSubmonoid_mono`, `toSubmonoid_strictMono`, `topEquiv_apply`, `topEquiv_symm_apply_coe`, `top_prod`, `top_prod_top`, `instCharZero`	151
Total	191

RingEquiv

Definitions

Name	Category	Theorems
`ofLeftInverseS` 📖	CompOp	2 math math: `ofLeftInverseS_symm_apply`, `ofLeftInverseS_apply`
`subsemiringCongr` 📖	CompOp	—
`subsemiringMap` 📖	CompOp	2 math math: `subsemiringMap_apply_coe`, `subsemiringMap_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLeftInverseS_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `ofLeftInverseS`	—	—
`ofLeftInverseS_symm_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`RingEquiv` `Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `ofLeftInverseS`	—	—
`subsemiringMap_apply_coe` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.map` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `RingEquivClass.toRingHomClass` `instRingEquivClass` `DFunLike.coe` `Subsemiring.toNonAssocSemiring` `subsemiringMap`	—	`RingEquivClass.toRingHomClass` `instRingEquivClass`
`subsemiringMap_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `DFunLike.coe` `RingEquiv` `Subsemiring.map` `RingHomClass.toRingHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `RingEquivClass.toRingHomClass` `instRingEquivClass` `Subsemiring.toNonAssocSemiring` `symm` `subsemiringMap` `toRingHom`	—	`RingEquivClass.toRingHomClass` `instRingEquivClass`

RingHom

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	5 math math: `surjective_codRestrict`, `rangeS_codRestrict`, `injective_codRestrict`, `IsLocalRing.exists_factor_valuationRing`, `codRestrict_apply`
`fintypeRangeS` 📖	CompOp	—
`rangeS` 📖	CompOp	39 math math: `Subring.range_snd`, `surjective_codRestrict`, `rangeS_eq_top`, `RingCon.rangeS_kerLift`, `rangeS_codRestrict`, `rangeSRestrict_surjective`, `RingEquiv.ofLeftInverseS_symm_apply`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `rangeS_toSubmonoid`, `RingCon.comapQuotientEquivRangeS_symm_mk`, `coe_rangeSRestrict`, `isArtinianRing_rangeS`, `Polynomial.lifts_iff_ringHom_rangeS`, `Subsemiring.map_comap_eq`, `RingCon.comapQuotientEquivRangeS_mk`, `RingCon.coe_quotientKerEquivRangeS_mk`, `Subsemiring.rangeS_subtype`, `rangeS_eq_map`, `Subsemiring.range_fst`, `mem_rangeS`, `rangeS_top_iff_surjective`, `StarSubalgebra.rangeS_le`, `rangeS_top_of_surjective`, `mem_rangeS_self`, `Subsemiring.range_snd`, `isNoetherianRing_rangeS`, `Subalgebra.rangeS_algebraMap`, `NonUnitalNonAssocSemiring.mem_center_iff`, `RingCon.rangeS_mk'`, `Subring.range_fst`, `RingEquiv.ofLeftInverseS_apply`, `Subalgebra.mem_perfectClosure_iff`, `RingCon.rangeS_lift`, `map_rangeS`, `Subalgebra.rangeS_le`, `Polynomial.mem_map_rangeS`, `AlgHom.range_toSubsemiring`, `coe_rangeS`, `ker_rangeSRestrict`
`rangeSRestrict` 📖	CompOp	3 math math: `rangeSRestrict_surjective`, `coe_rangeSRestrict`, `ker_rangeSRestrict`
`restrict` 📖	CompOp	2 math math: `comp_restrict`, `coe_restrict_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codRestrict_apply` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`SubsemiringClass.toNonAssocSemiring` `codRestrict`	—	—
`coe_rangeS` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Subsemiring.instSetLike` `rangeS` `Set.range` `DFunLike.coe` `RingHom` `instFunLike`	—	—
`coe_rangeSRestrict` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `rangeS` `DFunLike.coe` `RingHom` `Subsemiring.toNonAssocSemiring` `instFunLike` `rangeSRestrict`	—	—
`coe_restrict_apply` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`SubsemiringClass.toNonAssocSemiring` `restrict`	—	—
`comp_restrict` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`comp` `SubsemiringClass.toNonAssocSemiring` `SubsemiringClass.subtype` `restrict`	—	—
`eqOn_sclosure` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `RingHom` `instFunLike`	`SetLike.coe` `Subsemiring` `Subsemiring.instSetLike` `Subsemiring.closure`	—	`Subsemiring.closure_le`
`eq_of_eqOn_sdense` 📖	—	`Subsemiring.closure` `Top.top` `Subsemiring` `Subsemiring.instTop` `Set.EqOn` `DFunLike.coe` `RingHom` `instFunLike`	—	—	`eq_of_eqOn_stop` `eqOn_sclosure`
`eq_of_eqOn_stop` 📖	—	`Set.EqOn` `DFunLike.coe` `RingHom` `instFunLike` `SetLike.coe` `Subsemiring` `Subsemiring.instSetLike` `Top.top` `Subsemiring.instTop`	—	—	`ext` `Subsemiring.mem_top`
`injective_codRestrict` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`SubsemiringClass.toNonAssocSemiring` `codRestrict`	—	`Set.injective_codRestrict`
`map_closureS` 📖	mathematical	—	`Subsemiring.map` `Subsemiring.closure` `Set.image` `DFunLike.coe` `RingHom` `instFunLike`	—	`GaloisConnection.l_comm_of_u_comm` `Set.image_preimage` `Subsemiring.gc_map_comap` `GaloisInsertion.gc` `Subsemiring.coe_comap`
`map_rangeS` 📖	mathematical	—	`Subsemiring.map` `rangeS` `comp`	—	`rangeS_eq_map` `Subsemiring.map_map`
`mem_rangeS` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `rangeS` `DFunLike.coe` `RingHom` `instFunLike`	—	—
`mem_rangeS_self` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `rangeS` `DFunLike.coe` `RingHom` `instFunLike`	—	`mem_rangeS`
`rangeSRestrict_surjective` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `rangeS` `DFunLike.coe` `RingHom` `Subsemiring.toNonAssocSemiring` `instFunLike` `rangeSRestrict`	—	`mem_rangeS`
`rangeS_codRestrict` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`rangeS` `SubsemiringClass.toNonAssocSemiring` `codRestrict` `Subsemiring.comap` `SubsemiringClass.subtype`	—	`SetLike.coe_injective` `Set.range_codRestrict`
`rangeS_eq_map` 📖	mathematical	—	`rangeS` `Subsemiring.map` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	`Subsemiring.ext`
`rangeS_eq_top` 📖	mathematical	—	`rangeS` `Top.top` `Subsemiring` `Subsemiring.instTop` `DFunLike.coe` `RingHom` `instFunLike`	—	—
`rangeS_toSubmonoid` 📖	mathematical	—	`Subsemiring.toSubmonoid` `rangeS` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul` `MulOneClass.toMulOne` `Set.range` `DFunLike.coe` `RingHom` `instFunLike` `Subsemiring.map` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	—
`rangeS_top_iff_surjective` 📖	mathematical	—	`rangeS` `Top.top` `Subsemiring` `Subsemiring.instTop` `DFunLike.coe` `RingHom` `instFunLike`	—	`SetLike.ext'_iff` `coe_rangeS` `Subsemiring.coe_top` `Set.range_eq_univ`
`rangeS_top_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`rangeS` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	`rangeS_top_iff_surjective`
`sclosure_preimage_le` 📖	mathematical	—	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subsemiring.instPartialOrder` `Subsemiring.closure` `Set.preimage` `DFunLike.coe` `RingHom` `instFunLike` `Subsemiring.comap`	—	`Subsemiring.closure_le` `SetLike.mem_coe` `Subsemiring.mem_comap` `Subsemiring.subset_closure`
`surjective_codRestrict` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `instFunLike`	`SubsemiringClass.toNonAssocSemiring` `codRestrict` `rangeS` `Subsemiring.ofClass`	—	`Set.surjective_codRestrict` `SetLike.coe_set_eq`

Submonoid

Definitions

Name	Category	Theorems
`subsemiringClosure` 📖	CompOp	5 math math: `subsemiringClosure_toAddSubmonoid`, `subsemiringClosure_eq_closure`, `subsemiringClosure_coe`, `subsemiringClosure_mem`, `subsemiringClosure_toNonUnitalSubsemiring`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsemiringClosure_coe` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Subsemiring.instSetLike` `subsemiringClosure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instSetLike`	—	—
`subsemiringClosure_eq_closure` 📖	mathematical	—	`subsemiringClosure` `Subsemiring.closure` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instSetLike`	—	`Subsemiring.ext` `AddSubmonoid.mem_closure` `Subsemiring.mem_closure`
`subsemiringClosure_mem` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `subsemiringClosure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instSetLike`	—	—
`subsemiringClosure_toAddSubmonoid` 📖	mathematical	—	`Subsemiring.toAddSubmonoid` `subsemiringClosure` `AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instSetLike`	—	—
`subsemiringClosure_toNonUnitalSubsemiring` 📖	mathematical	—	`Subsemiring.toNonUnitalSubsemiring` `subsemiringClosure` `NonUnitalSubsemiring.closure` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instSetLike`	—	`NonUnitalSubsemiring.closure_eq_of_le` `AddSubmonoid.closure_induction` `NonUnitalSubsemiring.mem_closure_of_mem` `AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass`

Subsemiring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	21 math math: `CentroidHom.star_centerToCentroidCenter`, `Subalgebra.center_toSubsemiring`, `center_eq_top`, `centerCongr_symm_apply_coe`, `Matrix.subsemiringCenter_eq_scalar_map`, `centerCongr_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_toSubmonoid`, `centerToMulOpposite_apply_coe`, `Subring.center_toSubsemiring`, `center.smulCommClass_right`, `instSMulCommClassSubtypeMemCenter_1`, `instSMulCommClassSubtypeMemCenter`, `centralizer_eq_top_iff_subset`, `CentroidHom.centerToCentroidCenter_apply`, `centralizer_univ`, `coe_center`, `Module.End.mem_subsemiringCenter_iff`, `mem_center_iff`, `center_le_centralizer`, `center.smulCommClass_left`
`centerCongr` 📖	CompOp	2 math math: `centerCongr_symm_apply_coe`, `centerCongr_apply_coe`
`centerToMulOpposite` 📖	CompOp	2 math math: `centerToMulOpposite_symm_apply_coe`, `centerToMulOpposite_apply_coe`
`centralizer` 📖	CompOp	12 math math: `centralizer_le`, `Subring.centralizer_toSubsemiring`, `centralizer_centralizer_centralizer`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `closure_le_centralizer_centralizer`, `mem_centralizer_iff`, `centralizer_toSubmonoid`, `coe_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_univ`, `le_centralizer_centralizer`, `center_le_centralizer`
`closure` 📖	CompOp	36 math math: `closure_le`, `closure_addSubmonoid_closure`, `closure_insert_natCast`, `closure_mono`, `closure_insert_zero`, `mem_closure`, `Submonoid.subsemiringClosure_eq_closure`, `closure_isSquare`, `closure_insert_one`, `unop_closure`, `op_closure`, `subset_closure`, `closure_le_centralizer_centralizer`, `closure_singleton_one`, `IsHomogeneous.subsemiringClosure`, `closure_singleton_natCast`, `RingHom.map_closureS`, `closure_iUnion`, `closure_sUnion`, `closure_eq`, `RingHom.sclosure_preimage_le`, `mem_closure_iff_exists_list`, `coe_closure_eq`, `closure_empty`, `closure_univ`, `closure_union`, `NonUnitalSubsemiring.unitization_range`, `closure_submonoid_closure`, `Algebra.adjoin_toSubsemiring`, `smul_closure`, `closure_singleton_zero`, `mem_closure_of_mem`, `RingHom.eqOn_sclosure`, `IsHomogeneous.subsemiringClosure_of_isHomogeneousElem`, `mem_closure_iff`, `Algebra.adjoin_nat`
`closureCommSemiringOfComm` 📖	CompOp	—
`comap` 📖	CompOp	20 math math: `comap_iInf`, `gc_map_comap`, `RingHom.rangeS_codRestrict`, `prod_top`, `map_comap_eq_self`, `comap_comap`, `comap_top`, `map_comap_eq`, `comap_toSubmonoid`, `mem_comap`, `RingHom.sclosure_preimage_le`, `Subalgebra.comap_toSubsemiring`, `comap_inf`, `map_comap_eq_self_of_surjective`, `map_le_iff_le_comap`, `map_equiv_eq_comap_symm`, `top_prod`, `comap_equiv_eq_map_symm`, `comap_map_eq_self_of_injective`, `coe_comap`
`decidableMemCenter` 📖	CompOp	—
`distribMulAction` 📖	CompOp	—
`equivMapOfInjective` 📖	CompOp	1 math math: `coe_equivMapOfInjective_apply`
`gi` 📖	CompOp	—
`inclusion` 📖	CompOp	1 math math: `inclusion_injective`
`instBot` 📖	CompOp	13 math math: `op_eq_bot`, `mem_bot`, `map_bot`, `smul_bot`, `closure_singleton_one`, `closure_singleton_natCast`, `closure_empty`, `prod_bot_sup_bot_prod`, `unop_bot`, `unop_eq_bot`, `closure_singleton_zero`, `coe_bot`, `op_bot`
`instCompleteLattice` 📖	CompOp	20 math math: `mem_sSup_of_directedOn`, `map_sup`, `op_sup`, `mem_iSup_of_directed`, `coe_iSup_of_directed`, `op_iSup`, `unop_sup`, `Algebra.sup_toSubsemiring`, `Algebra.iSup_toSubsemiring`, `Algebra.sSup_toSubsemiring`, `closure_iUnion`, `closure_sUnion`, `map_iSup`, `op_sSup`, `coe_sSup_of_directedOn`, `closure_union`, `prod_bot_sup_bot_prod`, `smul_sup`, `unop_sSup`, `unop_iSup`
`instInfSet` 📖	CompOp	14 math math: `comap_iInf`, `mem_iInf`, `map_iInf`, `op_sInf`, `Algebra.sInf_toSubsemiring`, `coe_sInf`, `unop_sInf`, `sInf_toAddSubmonoid`, `Algebra.iInf_toSubsemiring`, `unop_iInf`, `sInf_toSubmonoid`, `coe_iInf`, `op_iInf`, `mem_sInf`
`instInhabited` 📖	CompOp	—
`instModuleSubtypeMem` 📖	CompOp	—
`instMulActionWithZeroSubtypeMem` 📖	CompOp	—
`instMulSemiringActionSubtypeMem` 📖	CompOp	—
`instSMulWithZeroSubtypeMem` 📖	CompOp	—
`instSMulWithZeroSubtypeMem_1` 📖	CompOp	—
`map` 📖	CompOp	29 math math: `map_map`, `map_sup`, `gc_map_comap`, `map_iInf`, `map_bot`, `RingHom.rangeS_toSubmonoid`, `coe_equivMapOfInjective_apply`, `map_comap_eq_self`, `Matrix.subsemiringCenter_eq_scalar_map`, `mem_map_equiv`, `RingEquiv.subsemiringMap_apply_coe`, `map_comap_eq`, `RingHom.map_closureS`, `map_id`, `RingEquiv.subsemiringMap_symm_apply_coe`, `RingHom.rangeS_eq_map`, `map_inf`, `pointwise_smul_def`, `map_comap_eq_self_of_surjective`, `map_iSup`, `map_toSubmonoid`, `mem_map`, `map_le_iff_le_comap`, `map_equiv_eq_comap_symm`, `comap_equiv_eq_map_symm`, `RingHom.map_rangeS`, `comap_map_eq_self_of_injective`, `coe_map`, `Subalgebra.map_toSubsemiring`
`mulAction` 📖	CompOp	—
`mulActionWithZero` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`prod` 📖	CompOp	9 math math: `coe_prod`, `prod_top`, `prod_mono_right`, `top_prod_top`, `prod_mono_left`, `prod_bot_sup_bot_prod`, `top_prod`, `mem_prod`, `prod_mono`
`prodEquiv` 📖	CompOp	—
`smul` 📖	CompOp	11 math math: `IsScalarTower.subsemiring`, `isScalarTower`, `smul_def`, `center.smulCommClass_right`, `instSMulCommClassSubtypeMemCenter_1`, `smulCommClass_left`, `instSMulCommClassSubtypeMemCenter`, `continuousSMul`, `smulCommClass_right`, `faithfulSMul`, `center.smulCommClass_left`
`topEquiv` 📖	CompOp	2 math math: `topEquiv_symm_apply_coe`, `topEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCongr_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subsemiring` `instSetLike` `center` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subsemiring` `instSetLike` `center` `toNonAssocSemiring` `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` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `Subsemiring` `instSetLike` `center` `MulOpposite.instNonAssocSemiring` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `MulOpposite` `Subsemiring` `MulOpposite.instNonAssocSemiring` `instSetLike` `center` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_eq_top` 📖	mathematical	—	`center` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Top.top` `Subsemiring` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`center_le_centralizer` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.center_subset_centralizer`
`center_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `center` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul` `MulOneClass.toMulOne` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `NonUnitalSubsemiring.center`	—	—
`centralizer_centralizer_centralizer` 📖	mathematical	—	`centralizer` `Set.centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`SetLike.coe_injective` `Set.centralizer_centralizer_centralizer`
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `Subsemiring` `Semiring.toNonAssocSemiring` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.centralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.centralizer_subset`
`centralizer_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `Semiring.toNonAssocSemiring` `centralizer` `Submonoid.centralizer` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center` `Semiring.toNonAssocSemiring`	—	`SetLike.ext'` `Set.centralizer_univ`
`closure_addSubmonoid_closure` 📖	mathematical	—	`closure` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	`ext` `AddSubmonoid.mem_closure` `mem_closure_iff` `Submonoid.mem_closure` `closure_mono` `AddSubmonoid.subset_closure`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `Subsemiring` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `Subsemiring` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subsemiring` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `Subsemiring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ZeroMemClass.zero_mem` `Subsemiring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `closure` `AddMonoidWithOne.toOne` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `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` `instSubsemiringClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ZeroMemClass.zero_mem` `Subsemiring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `closure` `AddMonoidWithOne.toOne` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `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` `instSubsemiringClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `closure_induction`
`closure_insert_natCast` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Set.insert_eq` `closure_union` `closure_singleton_natCast` `sup_of_le_right`
`closure_insert_one` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.cast_one` `closure_insert_natCast`
`closure_insert_zero` 📖	mathematical	—	`closure` `Set` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Nat.cast_zero` `closure_insert_natCast`
`closure_le` 📖	mathematical	—	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_centralizer_centralizer`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `iSup` `Subsemiring` `Set` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `GaloisInsertion.gc`
`closure_singleton_natCast` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Bot.bot` `Subsemiring` `instBot`	—	`bot_unique` `closure_le` `Set.singleton_subset_iff` `natCast_mem` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass`
`closure_singleton_one` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Bot.bot` `Subsemiring` `instBot`	—	`Nat.cast_one` `closure_singleton_natCast`
`closure_singleton_zero` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Bot.bot` `Subsemiring` `instBot`	—	`Nat.cast_zero` `closure_singleton_natCast`
`closure_submonoid_closure` 📖	mathematical	—	`closure` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.closure`	—	`le_antisymm` `closure_le` `Submonoid.mem_closure` `subset_closure` `closure_mono` `Submonoid.subset_closure`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `Subsemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `Subsemiring` `instTop`	—	`closure_eq` `coe_top`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `Bot.bot` `instBot` `Set.range` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHom.coe_rangeS`
`coe_center` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `center` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `NonUnitalSubsemiring.center`	—	—
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `instSetLike` `centralizer` `Set.centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`coe_closure_eq` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `closure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.closure`	—	`Submonoid.subsemiringClosure_eq_closure` `closure_submonoid_closure`
`coe_comap` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `comap` `Set.preimage` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—
`coe_equivMapOfInjective_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`Subsemiring` `SetLike.instMembership` `instSetLike` `map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivMapOfInjective`	—	—
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `mem_iSup_of_directed`
`coe_map` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `map` `Set.image` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Prod.instNonAssocSemiring` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subsemiring` `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`
`comap_comap` 📖	mathematical	—	`comap` `RingHom.comp`	—	—
`comap_equiv_eq_map_symm` 📖	mathematical	—	`comap` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map` `RingEquiv.symm`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_equiv_eq_comap_symm`
`comap_iInf` 📖	mathematical	—	`comap` `iInf` `Subsemiring` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_inf` 📖	mathematical	—	`comap` `Subsemiring` `instMin`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_map_eq_self_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`comap` `map`	—	`SetLike.coe_injective` `Set.preimage_image_eq`
`comap_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `comap` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul` `MulOneClass.toMulOne` `Set.preimage` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `SetLike.coe` `Subsemiring` `instSetLike`	—	—
`comap_top` 📖	mathematical	—	`comap` `Top.top` `Subsemiring` `instTop`	—	`GaloisConnection.u_top` `gc_map_comap`
`eq_top_iff'` 📖	mathematical	—	`Top.top` `Subsemiring` `instTop` `SetLike.instMembership` `instSetLike`	—	`eq_top_iff` `mem_top`
`faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `Subsemiring` `SetLike.instMembership` `instSetLike` `smul`	—	`instFaithfulSMulSubtypeMem`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `Subsemiring` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`inclusion_injective` 📖	mathematical	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `DFunLike.coe` `RingHom` `toNonAssocSemiring` `RingHom.instFunLike` `inclusion`	—	`Set.inclusion_injective`
`instFaithfulSMulSubtypeMem` 📖	mathematical	—	`FaithfulSMul` `SetLike.instMembership` `Submonoid.instSMulSubtypeMem`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`instSMulCommClassSubtypeMemCenter` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `center` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `smul`	—	`Submonoid.instSMulCommClassSubtypeMemCenter_1`
`instSMulCommClassSubtypeMemCenter_1` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `center` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Submonoid.instSMulCommClassSubtypeMemCenter`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Subsemiring` `SetLike.instMembership` `instSetLike` `smul`	—	`Submonoid.instIsScalarTowerSubtypeMem`
`le_centralizer_centralizer` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer` `SetLike.coe` `instSetLike`	—	`Set.subset_centralizer_centralizer`
`list_prod_mem` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`list_prod_mem` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass`
`list_sum_mem` 📖	mathematical	`Subsemiring` `SetLike.instMembership` `instSetLike`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`list_sum_mem` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass`
`map_bot` 📖	mathematical	—	`map` `Bot.bot` `Subsemiring` `instBot`	—	`GaloisConnection.l_bot` `gc_map_comap`
`map_comap_eq` 📖	mathematical	—	`map` `comap` `Subsemiring` `instMin` `RingHom.rangeS`	—	`SetLike.coe_injective` `Set.image_preimage_eq_inter_range`
`map_comap_eq_self` 📖	mathematical	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RingHom.rangeS`	`map` `comap`	—	`inf_of_le_left` `map_comap_eq`
`map_comap_eq_self_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`map` `comap`	—	`map_comap_eq_self` `RingHom.rangeS_top_of_surjective`
`map_equiv_eq_comap_symm` 📖	mathematical	—	`map` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `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` `RingHom.instFunLike`	`map` `iInf` `Subsemiring` `instInfSet`	—	`SetLike.coe_injective` `coe_iInf` `Set.InjOn.image_iInter_eq` `Set.injOn_of_injective`
`map_iSup` 📖	mathematical	—	`map` `iSup` `Subsemiring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_id` 📖	mathematical	—	`map` `RingHom.id`	—	`SetLike.coe_injective` `Set.image_id`
`map_inf` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`map` `Subsemiring` `instMin`	—	`SetLike.coe_injective` `Set.image_inter`
`map_le_iff_le_comap` 📖	mathematical	—	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `RingHom.comp`	—	`SetLike.coe_injective` `Set.image_image`
`map_sup` 📖	mathematical	—	`map` `Subsemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`map_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `map` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul` `MulOneClass.toMulOne` `Set.image` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `SetLike.coe` `Subsemiring` `instSetLike`	—	—
`mem_bot` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHom.mem_rangeS`
`mem_center_iff` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Subsemigroup.mem_center_iff`
`mem_centralizer_iff` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`mem_closure` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `closure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.closure`	—	`Set.ext_iff` `coe_closure_eq`
`mem_closure_iff_exists_list` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `instSetLike` `closure` `Set` `Set.instMembership` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`AddSubmonoid.closure_induction` `Submonoid.closure_induction` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `mem_closure_iff` `list_sum_mem` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `list_prod_mem` `subset_closure`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Subsemiring` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—
`mem_iInf` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup_of_directed` 📖	mathematical	`Directed` `Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`Submonoid.coe_iSup_of_directed` `AddSubmonoid.coe_iSup_of_directed` `iSup_le` `Set.mem_iUnion` `le_iSup`
`mem_map` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—
`mem_map_equiv` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `map` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `DFunLike.coe` `RingEquiv.symm`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Set.mem_image_equiv`
`mem_prod` 📖	mathematical	—	`Subsemiring` `Prod.instNonAssocSemiring` `SetLike.instMembership` `instSetLike` `prod`	—	—
`mem_sInf` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subsemiring` `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`
`multiset_prod_mem` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike`	`Multiset.prod` `CommSemiring.toCommMonoid`	—	`multiset_prod_mem` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass`
`multiset_sum_mem` 📖	mathematical	`Subsemiring` `SetLike.instMembership` `instSetLike`	`Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`multiset_sum_mem` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass`
`notMem_of_notMem_closure` 📖	mathematical	`Subsemiring` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`prod_bot_sup_bot_prod` 📖	mathematical	—	`Subsemiring` `Prod.instNonAssocSemiring` `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` `instSubsemiringClass` `le_sup_left` `SetLike.mem_coe` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `le_sup_right` `Prod.fst_mul_snd`
`prod_mem` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike`	`Finset.prod` `CommSemiring.toCommMonoid`	—	`prod_mem` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass`
`prod_mono` 📖	mathematical	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instNonAssocSemiring` `prod`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	—	`Monotone` `Subsemiring` `Prod.instNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_mono_right` 📖	mathematical	—	`Monotone` `Subsemiring` `Prod.instNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_top` 📖	mathematical	—	`prod` `Top.top` `Subsemiring` `instTop` `comap` `Prod.instNonAssocSemiring` `RingHom.fst`	—	`ext`
`rangeS_subtype` 📖	mathematical	—	`RingHom.rangeS` `Subsemiring` `SetLike.instMembership` `instSetLike` `toNonAssocSemiring` `subtype`	—	`SetLike.coe_injective` `RingHom.coe_rangeS` `Subtype.range_coe`
`range_fst` 📖	mathematical	—	`RingHom.rangeS` `Prod.instNonAssocSemiring` `RingHom.fst` `Top.top` `Subsemiring` `instTop`	—	`RingHom.rangeS_top_of_surjective` `Prod.fst_surjective` `Zero.instNonempty`
`range_snd` 📖	mathematical	—	`RingHom.rangeS` `Prod.instNonAssocSemiring` `RingHom.snd` `Top.top` `Subsemiring` `instTop`	—	`RingHom.rangeS_top_of_surjective` `Prod.snd_surjective` `Zero.instNonempty`
`sInf_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `InfSet.sInf` `Subsemiring` `instInfSet` `iInf` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.instInfSet` `Set` `Set.instMembership`	—	`mk'_toAddSubmonoid`
`sInf_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `InfSet.sInf` `Subsemiring` `instInfSet` `iInf` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instInfSet` `Set` `Set.instMembership`	—	`mk'_toSubmonoid`
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `SetLike.instMembership` `instSetLike` `smul`	—	`Submonoid.instSMulCommClassSubtypeMem`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `SetLike.instMembership` `instSetLike` `smul`	—	`Submonoid.instSMulCommClassSubtypeMem_1`
`smul_def` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `smul`	—	—
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subsemiring` `instSetLike` `closure`	—	`mem_closure`
`sum_mem` 📖	mathematical	`Subsemiring` `SetLike.instMembership` `instSetLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`sum_mem` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass`
`toAddSubmonoid_mono` 📖	mathematical	—	`Monotone` `Subsemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `PartialOrder.toPreorder` `instPartialOrder` `AddSubmonoid.instPartialOrder` `toAddSubmonoid`	—	`StrictMono.monotone` `toAddSubmonoid_strictMono`
`toAddSubmonoid_strictMono` 📖	mathematical	—	`StrictMono` `Subsemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `PartialOrder.toPreorder` `instPartialOrder` `AddSubmonoid.instPartialOrder` `toAddSubmonoid`	—	—
`toSubmonoid_mono` 📖	mathematical	—	`Monotone` `Subsemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `PartialOrder.toPreorder` `instPartialOrder` `Submonoid.instPartialOrder` `toSubmonoid`	—	`StrictMono.monotone` `toSubmonoid_strictMono`
`toSubmonoid_strictMono` 📖	mathematical	—	`StrictMono` `Subsemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `PartialOrder.toPreorder` `instPartialOrder` `Submonoid.instPartialOrder` `toSubmonoid`	—	—
`topEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Subsemiring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `topEquiv`	—	—
`topEquiv_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `topEquiv`	—	—
`top_prod` 📖	mathematical	—	`prod` `Top.top` `Subsemiring` `instTop` `comap` `Prod.instNonAssocSemiring` `RingHom.snd`	—	`ext`
`top_prod_top` 📖	mathematical	—	`prod` `Top.top` `Subsemiring` `instTop` `Prod.instNonAssocSemiring`	—	`top_prod` `comap_top`

Subsemiring.center

Definitions

Name	Category	Theorems
`commSemiring` 📖	CompOp	—
`commSemiring'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.center` `Subsemiring.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Submonoid.center.smulCommClass_left`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.center` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.smul`	—	`Submonoid.center.smulCommClass_right`

SubsemiringClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCharZero` 📖	mathematical	—	`CharZero` `SetLike.instMembership` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `toNonAssocSemiring`	—	`Function.Injective.of_comp` `Nat.cast_injective`

---

← Back to Index