Basic

📁 Source: Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Statistics

Metric	Count
Definitions `srange`, `srangeRestrict`, `center`, `instNonUnitalCommSemiring`, `centerCongr`, `centerToMulOpposite`, `centralizer`, `closure`, `closureNonUnitalCommSemiringOfComm`, `comap`, `decidableMemCenter`, `equivMapOfInjective`, `gi`, `instCompleteLattice`, `instInfSet`, `map`, `prod`, `prodEquiv`, `topEquiv`, `nonUnitalSubsemiringCongr`, `nonUnitalSubsemiringMap`, `sofLeftInverse'`, `nonUnitalSubsemiringClosure`	23
Theorems `coe_srange`, `coe_srangeRestrict`, `eqOn_sclosure`, `eq_of_eqOn_sdense`, `eq_of_eqOn_stop`, `finite_srange`, `map_sclosure`, `map_srange`, `mem_srange`, `mem_srange_self`, `sclosure_preimage_le`, `srangeRestrict_surjective`, `srange_eq_map`, `srange_eq_top_iff_surjective`, `srange_eq_top_of_surjective`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_eq_top`, `center_le_centralizer`, `center_toSubsemigroup`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toSubsemigroup`, `centralizer_univ`, `closure_addSubmonoid_closure`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_le`, `closure_le_centralizer_centralizer`, `closure_mono`, `closure_sUnion`, `closure_subsemigroup_closure`, `closure_union`, `closure_univ`, `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_top`, `eq_top_iff'`, `gc_map_comap`, `map_bot`, `map_equiv_eq_comap_symm`, `map_iInf`, `map_iSup`, `map_id`, `map_inf`, `map_le_iff_le_comap`, `map_map`, `map_sup`, `mem_center_iff`, `mem_centralizer_iff`, `mem_closure`, `mem_closure_iff`, `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`, `notMem_of_notMem_closure`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_top`, `range_fst`, `range_snd`, `sInf_toAddSubmonoid`, `sInf_toSubsemigroup`, `srange_subtype`, `subset_closure`, `toAddSubmonoid_mono`, `toAddSubmonoid_strictMono`, `toSubsemigroup_mono`, `toSubsemigroup_strictMono`, `topEquiv_apply`, `topEquiv_symm_apply_coe`, `top_prod`, `top_prod_top`, `nonUnitalSubsemiringMap_apply_coe`, `nonUnitalSubsemiringMap_symm_apply_coe`, `sofLeftInverse'_apply`, `sofLeftInverse'_symm_apply`, `mem_center_iff_addMonoidHom`, `nonUnitalSubsemiringClosure_coe`, `nonUnitalSubsemiringClosure_eq_closure`, `nonUnitalSubsemiringClosure_toAddSubmonoid`	107
Total	130

NonUnitalRingHom

Definitions

Name	Category	Theorems
`srange` 📖	CompOp	17 math math: `NonUnitalSubsemiring.srange_subtype`, `srange_eq_map`, `mem_srange`, `mem_srange_self`, `RingEquiv.sofLeftInverse'_apply`, `NonUnitalSubring.range_snd`, `srangeRestrict_surjective`, `srange_eq_top_iff_surjective`, `NonUnitalSubsemiring.range_fst`, `map_srange`, `srange_eq_top_of_surjective`, `RingEquiv.sofLeftInverse'_symm_apply`, `finite_srange`, `coe_srange`, `coe_srangeRestrict`, `NonUnitalSubsemiring.range_snd`, `NonUnitalSubring.range_fst`
`srangeRestrict` 📖	CompOp	2 math math: `srangeRestrict_surjective`, `coe_srangeRestrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_srange` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `srange` `Set.range` `DFunLike.coe`	—	—
`coe_srangeRestrict` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `srange` `DFunLike.coe` `NonUnitalRingHom` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `instFunLike` `srangeRestrict`	—	`NonUnitalSubsemiring.instNonUnitalSubsemiringClass`
`eqOn_sclosure` 📖	mathematical	`Set.EqOn` `DFunLike.coe`	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.closure`	—	`NonUnitalSubsemiring.closure_le`
`eq_of_eqOn_sdense` 📖	—	`NonUnitalSubsemiring.closure` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop` `Set.EqOn` `DFunLike.coe`	—	—	`eq_of_eqOn_stop` `eqOn_sclosure`
`eq_of_eqOn_stop` 📖	—	`Set.EqOn` `DFunLike.coe` `SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `Top.top` `NonUnitalSubsemiring.instTop`	—	—	`DFunLike.ext`
`finite_srange` 📖	mathematical	—	`Finite` `NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `srange`	—	`Set.Finite.to_subtype` `Set.finite_range`
`map_sclosure` 📖	mathematical	—	`NonUnitalSubsemiring.map` `NonUnitalSubsemiring.closure` `Set.image` `DFunLike.coe`	—	`GaloisConnection.l_comm_of_u_comm` `Set.image_preimage` `NonUnitalSubsemiring.gc_map_comap` `GaloisInsertion.gc`
`map_srange` 📖	mathematical	—	`NonUnitalSubsemiring.map` `NonUnitalRingHom` `instFunLike` `instNonUnitalRingHomClass` `srange` `comp`	—	`instNonUnitalRingHomClass` `NonUnitalSubsemiring.map.congr_simp` `srange_eq_map` `NonUnitalSubsemiring.map_map`
`mem_srange` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `srange` `DFunLike.coe`	—	—
`mem_srange_self` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `srange` `DFunLike.coe`	—	`mem_srange`
`sclosure_preimage_le` 📖	mathematical	—	`NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalSubsemiring.instPartialOrder` `NonUnitalSubsemiring.closure` `Set.preimage` `DFunLike.coe` `NonUnitalSubsemiring.comap`	—	`NonUnitalSubsemiring.closure_le` `SetLike.mem_coe` `NonUnitalSubsemiring.mem_comap` `NonUnitalSubsemiring.subset_closure`
`srangeRestrict_surjective` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `srange` `DFunLike.coe` `NonUnitalRingHom` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `instFunLike` `srangeRestrict`	—	`NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `mem_srange`
`srange_eq_map` 📖	mathematical	—	`srange` `NonUnitalSubsemiring.map` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop`	—	`NonUnitalSubsemiring.ext`
`srange_eq_top_iff_surjective` 📖	mathematical	—	`srange` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop` `DFunLike.coe`	—	`SetLike.ext'_iff` `coe_srange` `NonUnitalSubsemiring.coe_top` `Set.range_eq_univ`
`srange_eq_top_of_surjective` 📖	mathematical	`DFunLike.coe`	`srange` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop`	—	`srange_eq_top_iff_surjective`

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	21 math math: `CentroidHom.star_centerToCentroidCenter`, `Subalgebra.coe_center`, `centerCongr_symm_apply_coe`, `centralizer_univ`, `centerToMulOpposite_symm_apply_coe`, `center_eq_top`, `coe_center`, `Subsemiring.center_toSubmonoid`, `NonUnitalNonAssocCommSemiring.mem_center_iff`, `NonUnitalSubring.center_toNonUnitalSubsemiring`, `NonUnitalSubalgebra.center_toNonUnitalSubsemiring`, `mem_center_iff`, `NonUnitalNonAssocSemiring.mem_center_iff`, `centralizer_eq_top_iff_subset`, `centerToMulOpposite_apply_coe`, `CentroidHom.centerToCentroidCenter_apply`, `center_le_centralizer`, `CentroidHom.centerToCentroid_apply`, `center_toSubsemigroup`, `centerCongr_apply_coe`, `Subsemiring.coe_center`
`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	8 math math: `centralizer_univ`, `closure_le_centralizer_centralizer`, `coe_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_toSubsemigroup`, `center_le_centralizer`, `centralizer_le`, `mem_centralizer_iff`
`closure` 📖	CompOp	23 math math: `mem_closure_of_mem`, `subset_closure`, `closure_union`, `closure_empty`, `closure_addSubmonoid_closure`, `closure_le_centralizer_centralizer`, `closure_mono`, `NonUnitalRingHom.map_sclosure`, `NonUnitalRingHom.sclosure_preimage_le`, `closure_subsemigroup_closure`, `closure_univ`, `closure_sUnion`, `closure_iUnion`, `closure_le`, `mem_closure`, `NonUnitalAlgebra.adjoin_toSubmodule`, `closure_isSquare`, `mem_closure_iff`, `Submonoid.subsemiringClosure_toNonUnitalSubsemiring`, `coe_closure_eq`, `Subsemigroup.nonUnitalSubsemiringClosure_eq_closure`, `closure_eq`, `NonUnitalRingHom.eqOn_sclosure`
`closureNonUnitalCommSemiringOfComm` 📖	CompOp	—
`comap` 📖	CompOp	13 math math: `top_prod`, `comap_iInf`, `gc_map_comap`, `map_equiv_eq_comap_symm`, `NonUnitalRingHom.sclosure_preimage_le`, `comap_comap`, `map_le_iff_le_comap`, `comap_equiv_eq_map_symm`, `comap_inf`, `comap_top`, `mem_comap`, `prod_top`, `coe_comap`
`decidableMemCenter` 📖	CompOp	—
`equivMapOfInjective` 📖	CompOp	1 math math: `coe_equivMapOfInjective_apply`
`gi` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	9 math math: `mem_iSup_of_directed`, `closure_union`, `coe_iSup_of_directed`, `map_iSup`, `closure_sUnion`, `closure_iUnion`, `map_sup`, `coe_sSup_of_directedOn`, `mem_sSup_of_directedOn`
`instInfSet` 📖	CompOp	9 math math: `NonUnitalAlgebra.sInf_toNonUnitalSubsemiring`, `mem_iInf`, `comap_iInf`, `map_iInf`, `mem_sInf`, `sInf_toAddSubmonoid`, `coe_iInf`, `sInf_toSubsemigroup`, `coe_sInf`
`map` 📖	CompOp	21 math math: `NonUnitalRingHom.srange_eq_map`, `coe_map`, `coe_equivMapOfInjective_apply`, `mem_map_equiv`, `map_map`, `map_id`, `gc_map_comap`, `map_iInf`, `map_equiv_eq_comap_symm`, `NonUnitalRingHom.map_sclosure`, `map_iSup`, `NonUnitalSubalgebra.map_toNonUnitalSubsemiring`, `map_le_iff_le_comap`, `mem_map`, `comap_equiv_eq_map_symm`, `NonUnitalRingHom.map_srange`, `RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe`, `map_sup`, `map_inf`, `map_bot`, `RingEquiv.nonUnitalSubsemiringMap_apply_coe`
`prod` 📖	CompOp	8 math math: `top_prod`, `prod_mono`, `prod_mono_left`, `top_prod_top`, `coe_prod`, `prod_top`, `prod_mono_right`, `mem_prod`
`prodEquiv` 📖	CompOp	—
`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` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `instSetLike` `center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `center.instNonUnitalCommSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `instSetLike` `center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `center.instNonUnitalCommSemiring` `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` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `instSetLike` `center` `MulOpposite.instNonUnitalNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `center.instNonUnitalCommSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `MulOpposite` `NonUnitalSubsemiring` `MulOpposite.instNonUnitalNonAssocSemiring` `instSetLike` `center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `center.instNonUnitalCommSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_eq_top` 📖	mathematical	—	`center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `Top.top` `NonUnitalSubsemiring` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`center_le_centralizer` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.center_subset_centralizer`
`center_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `center` `Subsemigroup.center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.centralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.centralizer_subset`
`centralizer_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `centralizer` `Subsemigroup.centralizer` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`SetLike.ext'` `Set.centralizer_univ`
`closure_addSubmonoid_closure` 📖	mathematical	—	`closure` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	`ext` `AddSubmonoid.mem_closure` `mem_closure_iff` `Subsemigroup.mem_closure` `closure_mono` `AddSubmonoid.subset_closure`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `NonUnitalSubsemiring` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `NonUnitalSubsemiring` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `NonUnitalSubsemiring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `ZeroMemClass.zero_mem` `NonUnitalSubsemiring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass` `closure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `SetLike.instMembership`	—	—	`subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `ZeroMemClass.zero_mem` `NonUnitalSubsemiring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass` `closure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `SetLike.instMembership`	—	—	`subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `closure_induction`
`closure_le` 📖	mathematical	—	`NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_centralizer_centralizer`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `iSup` `NonUnitalSubsemiring` `Set` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `GaloisInsertion.gc`
`closure_subsemigroup_closure` 📖	mathematical	—	`closure` `SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `Subsemigroup.closure`	—	`le_antisymm` `closure_le` `Subsemigroup.mem_closure` `subset_closure` `closure_mono` `Subsemigroup.subset_closure`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `NonUnitalSubsemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `NonUnitalSubsemiring` `instTop`	—	`closure_eq` `coe_top`
`coe_center` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `center` `Set.center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instSetLike` `centralizer` `Set.centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coe_closure_eq` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `closure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `Subsemigroup.closure`	—	`Subsemigroup.nonUnitalSubsemiringClosure_eq_closure` `closure_subsemigroup_closure`
`coe_comap` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `comap` `Set.preimage` `DFunLike.coe`	—	—
`coe_equivMapOfInjective_apply` 📖	mathematical	`DFunLike.coe`	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivMapOfInjective`	—	`instNonUnitalSubsemiringClass`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `NonUnitalSubsemiring` `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` `NonUnitalSubsemiring` `instSetLike` `map` `Set.image` `DFunLike.coe`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `Prod.instNonUnitalNonAssocSemiring` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `NonUnitalSubsemiring` `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` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.comp` `NonUnitalRingHomClass.toNonUnitalRingHom`	—	—
`comap_equiv_eq_map_symm` 📖	mathematical	—	`comap` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHomClass.toNonUnitalRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `map` `RingEquiv.symm`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `map_equiv_eq_comap_symm`
`comap_iInf` 📖	mathematical	—	`comap` `iInf` `NonUnitalSubsemiring` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_inf` 📖	mathematical	—	`comap` `NonUnitalSubsemiring` `instMin`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_top` 📖	mathematical	—	`comap` `Top.top` `NonUnitalSubsemiring` `instTop`	—	`GaloisConnection.u_top` `gc_map_comap`
`eq_top_iff'` 📖	mathematical	—	`Top.top` `NonUnitalSubsemiring` `instTop` `SetLike.instMembership` `instSetLike`	—	`eq_top_iff` `mem_top`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `NonUnitalSubsemiring` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`map_bot` 📖	mathematical	—	`map` `Bot.bot` `NonUnitalSubsemiring` `instBot`	—	`GaloisConnection.l_bot` `gc_map_comap`
`map_equiv_eq_comap_symm` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHomClass.toNonUnitalRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `comap` `RingEquiv.symm`	—	`SetLike.coe_injective` `NonUnitalRingHom.instNonUnitalRingHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `Equiv.image_eq_preimage_symm`
`map_iInf` 📖	mathematical	`DFunLike.coe`	`map` `iInf` `NonUnitalSubsemiring` `instInfSet`	—	`SetLike.coe_injective` `coe_iInf` `Set.InjOn.image_iInter_eq` `Set.injOn_of_injective`
`map_iSup` 📖	mathematical	—	`map` `iSup` `NonUnitalSubsemiring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_id` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.id`	—	`SetLike.coe_injective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Set.image_id`
`map_inf` 📖	mathematical	`DFunLike.coe`	`map` `NonUnitalSubsemiring` `instMin`	—	`SetLike.coe_injective` `Set.image_inter`
`map_le_iff_le_comap` 📖	mathematical	—	`NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHomClass.toNonUnitalRingHom` `NonUnitalRingHom.comp`	—	`SetLike.coe_injective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Set.image_image`
`map_sup` 📖	mathematical	—	`map` `NonUnitalSubsemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`mem_center_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Semigroup.mem_center_iff`
`mem_centralizer_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mem_closure` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `closure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `Subsemigroup.closure`	—	`Set.ext_iff` `coe_closure_eq`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe`	—	—
`mem_iInf` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup_of_directed` 📖	mathematical	`Directed` `NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`Subsemigroup.coe_iSup_of_directed` `AddSubmonoid.coe_iSup_of_directed` `iSup_le` `Set.mem_iUnion` `le_iSup`
`mem_map` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe`	—	—
`mem_map_equiv` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHomClass.toNonUnitalRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `DFunLike.coe` `RingEquiv.symm`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `Set.mem_image_equiv`
`mem_prod` 📖	mathematical	—	`NonUnitalSubsemiring` `Prod.instNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `prod`	—	—
`mem_sInf` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `NonUnitalSubsemiring` `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`
`notMem_of_notMem_closure` 📖	mathematical	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`prod_mono` 📖	mathematical	`NonUnitalSubsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instNonUnitalNonAssocSemiring` `prod`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	—	`Monotone` `NonUnitalSubsemiring` `Prod.instNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_mono_right` 📖	mathematical	—	`Monotone` `NonUnitalSubsemiring` `Prod.instNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_top` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubsemiring` `instTop` `comap` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.fst`	—	`ext` `NonUnitalRingHom.instNonUnitalRingHomClass`
`range_fst` 📖	mathematical	—	`NonUnitalRingHom.srange` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.fst` `Top.top` `NonUnitalSubsemiring` `instTop`	—	`NonUnitalRingHom.srange_eq_top_of_surjective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Prod.fst_surjective` `Zero.instNonempty`
`range_snd` 📖	mathematical	—	`NonUnitalRingHom.srange` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.snd` `Top.top` `NonUnitalSubsemiring` `instTop`	—	`NonUnitalRingHom.srange_eq_top_of_surjective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Prod.snd_surjective` `Zero.instNonempty`
`sInf_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `InfSet.sInf` `NonUnitalSubsemiring` `instInfSet` `iInf` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instInfSet` `Set` `Set.instMembership`	—	`mk'_toAddSubmonoid`
`sInf_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `InfSet.sInf` `NonUnitalSubsemiring` `instInfSet` `iInf` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instInfSet` `Set` `Set.instMembership`	—	`mk'_toSubsemigroup`
`srange_subtype` 📖	mathematical	—	`NonUnitalRingHom.srange` `NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalSubsemiringClass.subtype`	—	`SetLike.coe_injective` `instNonUnitalSubsemiringClass` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.coe_srange` `Subtype.range_coe`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `closure`	—	`mem_closure`
`toAddSubmonoid_mono` 📖	mathematical	—	`Monotone` `NonUnitalSubsemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `AddSubmonoid.instPartialOrder` `toAddSubmonoid`	—	`StrictMono.monotone` `toAddSubmonoid_strictMono`
`toAddSubmonoid_strictMono` 📖	mathematical	—	`StrictMono` `NonUnitalSubsemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `AddSubmonoid.instPartialOrder` `toAddSubmonoid`	—	—
`toSubsemigroup_mono` 📖	mathematical	—	`Monotone` `NonUnitalSubsemiring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `PartialOrder.toPreorder` `instPartialOrder` `Subsemigroup.instPartialOrder` `toSubsemigroup`	—	`StrictMono.monotone` `toSubsemigroup_strictMono`
`toSubsemigroup_strictMono` 📖	mathematical	—	`StrictMono` `NonUnitalSubsemiring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `PartialOrder.toPreorder` `instPartialOrder` `Subsemigroup.instPartialOrder` `toSubsemigroup`	—	—
`topEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `topEquiv` `Subsemigroup` `Subsemigroup.instSetLike` `Subsemigroup.instTop`	—	`instNonUnitalSubsemiringClass`
`topEquiv_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.instMembership` `Subsemigroup.instSetLike` `Top.top` `Subsemigroup.instTop` `DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `instSetLike` `instTop` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `topEquiv`	—	`instNonUnitalSubsemiringClass`
`top_prod` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubsemiring` `instTop` `comap` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.snd`	—	`ext` `NonUnitalRingHom.instNonUnitalRingHomClass`
`top_prod_top` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubsemiring` `instTop` `Prod.instNonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `top_prod` `comap_top`

NonUnitalSubsemiring.center

Definitions

Name	Category	Theorems
`instNonUnitalCommSemiring` 📖	CompOp	7 math math: `CentroidHom.star_centerToCentroidCenter`, `NonUnitalSubsemiring.centerCongr_symm_apply_coe`, `NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe`, `NonUnitalSubsemiring.centerToMulOpposite_apply_coe`, `CentroidHom.centerToCentroidCenter_apply`, `CentroidHom.centerToCentroid_apply`, `NonUnitalSubsemiring.centerCongr_apply_coe`

RingEquiv

Definitions

Name	Category	Theorems
`nonUnitalSubsemiringCongr` 📖	CompOp	—
`nonUnitalSubsemiringMap` 📖	CompOp	2 math math: `nonUnitalSubsemiringMap_symm_apply_coe`, `nonUnitalSubsemiringMap_apply_coe`
`sofLeftInverse'` 📖	CompOp	2 math math: `sofLeftInverse'_apply`, `sofLeftInverse'_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonUnitalSubsemiringMap_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `EquivLike.toEquiv` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddEquiv.instEquivLike` `toAddEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `SetLike.coe` `AddSubmonoid` `AddSubmonoid.instSetLike` `NonUnitalSubsemiring.toAddSubmonoid` `RingEquiv` `NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `toNonUnitalRingHom` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `instEquivLike` `nonUnitalSubsemiringMap`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass`
`nonUnitalSubsemiringMap_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `NonUnitalSubsemiring.toAddSubmonoid` `DFunLike.coe` `RingEquiv` `NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.map` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `toNonUnitalRingHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `nonUnitalSubsemiringMap` `AddEquiv` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquivClass.toAddEquiv` `RingEquivClass.toAddEquivClass` `instRingEquivClass` `Set.image`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass`
`sofLeftInverse'_apply` 📖	mathematical	`DFunLike.coe`	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalRingHom.srange` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `sofLeftInverse'`	—	`NonUnitalSubsemiring.instNonUnitalSubsemiringClass`
`sofLeftInverse'_symm_apply` 📖	mathematical	`DFunLike.coe`	`RingEquiv` `NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalRingHom.srange` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `sofLeftInverse'`	—	`NonUnitalSubsemiring.instNonUnitalSubsemiringClass`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_center_iff_addMonoidHom` 📖	mathematical	—	`Set` `instMembership` `center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidHom.mulLeft` `AddMonoidHom.mulRight` `AddMonoidHom.compr₂` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.mul` `AddMonoidHom.comp` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instAddCommMonoid` `AddMonoidHom.compl₂`	—	`mem_center_iff` `isMulCentral_iff`

Subsemigroup

Definitions

Name	Category	Theorems
`nonUnitalSubsemiringClosure` 📖	CompOp	3 math math: `nonUnitalSubsemiringClosure_coe`, `nonUnitalSubsemiringClosure_toAddSubmonoid`, `nonUnitalSubsemiringClosure_eq_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonUnitalSubsemiringClosure_coe` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `nonUnitalSubsemiringClosure` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instSetLike`	—	—
`nonUnitalSubsemiringClosure_eq_closure` 📖	mathematical	—	`nonUnitalSubsemiringClosure` `NonUnitalSubsemiring.closure` `SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instSetLike`	—	`NonUnitalSubsemiring.ext` `AddSubmonoid.mem_closure` `NonUnitalSubsemiring.mem_closure`
`nonUnitalSubsemiringClosure_toAddSubmonoid` 📖	mathematical	—	`NonUnitalSubsemiring.toAddSubmonoid` `nonUnitalSubsemiringClosure` `AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instSetLike`	—	—

---

← Back to Index