Basic

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

Statistics

Metric	Count
Definitions `eqLocus`, `fintypeRange`, `range`, `rangeRestrict`, `center`, `instNonUnitalCommRing`, `centerCongr`, `centerToMulOpposite`, `centralizer`, `closure`, `closureNonUnitalCommRingOfComm`, `comap`, `decidableMemCenter`, `equivMapOfInjective`, `gi`, `instBot`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instMin`, `instTop`, `map`, `prod`, `prodEquiv`, `topEquiv`, `nonUnitalSubringCongr`, `ofLeftInverse'`	27
Theorems `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`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_eq_top`, `center_le_centralizer`, `center_toNonUnitalSubsemiring`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toNonUnitalSubsemiring`, `centralizer_univ`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_le`, `closure_le_centralizer_centralizer`, `closure_mono`, `closure_preimage_le`, `closure_sUnion`, `closure_union`, `closure_univ`, `coe_bot`, `coe_center`, `coe_centralizer`, `coe_comap`, `coe_equivMapOfInjective_apply`, `coe_iInf`, `coe_iSup_of_directed`, `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_top`, `eq_top_iff'`, `gc_map_comap`, `instIsMulCommutative_closure`, `isMulCommutative_closure`, `list_sum_mem`, `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_bot`, `mem_center_iff`, `mem_centralizer_iff`, `mem_closure`, `mem_closure_iff`, `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_sum_mem`, `notMem_of_notMem_closure`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_top`, `range_fst`, `range_snd`, `range_subtype`, `sInf_toAddSubgroup`, `sInf_toSubsemigroup`, `subset_closure`, `sum_mem`, `toAddSubgroup_eq_top`, `toAddSubgroup_top`, `toNonUnitalSubsemiring_eq_top`, `toNonUnitalSubsemiring_top`, `topEquiv_apply`, `topEquiv_symm_apply_coe`, `top_prod`, `top_prod_top`, `ofLeftInverse'_apply`, `ofLeftInverse'_symm_apply`	111
Total	138

NonUnitalRingHom

Definitions

Name	Category	Theorems
`eqLocus` 📖	CompOp	2 math math: `eqLocus_same`, `mem_eqLocus`
`fintypeRange` 📖	CompOp	—
`range` 📖	CompOp	12 math math: `mem_range`, `mem_range_self`, `range_eq_top`, `coe_range`, `RingEquiv.ofLeftInverse'_symm_apply`, `range_eq_top_of_surjective`, `RingEquiv.ofLeftInverse'_apply`, `coe_rangeRestrict`, `rangeRestrict_surjective`, `NonUnitalSubring.range_subtype`, `range_eq_map`, `map_range`
`rangeRestrict` 📖	CompOp	2 math math: `coe_rangeRestrict`, `rangeRestrict_surjective`

Theorems

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

NonUnitalSubring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	12 math math: `centerCongr_apply_coe`, `mem_center_iff`, `center_eq_top`, `centerCongr_symm_apply_coe`, `center_toNonUnitalSubsemiring`, `coe_center`, `centerToMulOpposite_symm_apply_coe`, `NonUnitalSubalgebra.center_toNonUnitalSubring`, `center_le_centralizer`, `centralizer_eq_top_iff_subset`, `centerToMulOpposite_apply_coe`, `centralizer_univ`
`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: `mem_centralizer_iff`, `centralizer_toNonUnitalSubsemiring`, `centralizer_le`, `coe_centralizer`, `Subring.centralizer_toNonUnitalSubring`, `center_le_centralizer`, `centralizer_eq_top_iff_subset`, `closure_le_centralizer_centralizer`, `centralizer_univ`
`closure` 📖	CompOp	20 math math: `mem_closure_of_mem`, `NonUnitalRingHom.map_closure`, `closure_preimage_le`, `closure_empty`, `NonUnitalRingHom.eqOn_set_closure`, `isMulCommutative_closure`, `closure_univ`, `closure_eq`, `closure_sUnion`, `closure_mono`, `closure_union`, `closure_iUnion`, `closure_eq_of_le`, `mem_closure_iff`, `subset_closure`, `mem_closure`, `instIsMulCommutative_closure`, `NonUnitalRingHom.closure_preimage_le`, `closure_le_centralizer_centralizer`, `closure_le`
`closureNonUnitalCommRingOfComm` 📖	CompOp	—
`comap` 📖	CompOp	14 math math: `prod_top`, `map_equiv_eq_comap_symm`, `closure_preimage_le`, `comap_top`, `comap_comap`, `map_le_iff_le_comap`, `top_prod`, `comap_equiv_eq_map_symm`, `mem_comap`, `comap_iInf`, `comap_inf`, `coe_comap`, `gc_map_comap`, `NonUnitalRingHom.closure_preimage_le`
`decidableMemCenter` 📖	CompOp	—
`equivMapOfInjective` 📖	CompOp	1 math math: `coe_equivMapOfInjective_apply`
`gi` 📖	CompOp	—
`instBot` 📖	CompOp	4 math math: `closure_empty`, `mem_bot`, `coe_bot`, `map_bot`
`instCompleteLattice` 📖	CompOp	9 math math: `map_iSup`, `mem_sSup_of_directedOn`, `mem_iSup_of_directed`, `map_sup`, `closure_sUnion`, `closure_union`, `coe_sSup_of_directedOn`, `closure_iUnion`, `coe_iSup_of_directed`
`instInfSet` 📖	CompOp	8 math math: `coe_sInf`, `coe_iInf`, `sInf_toSubsemigroup`, `mem_iInf`, `comap_iInf`, `sInf_toAddSubgroup`, `mem_sInf`, `map_iInf`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	4 math math: `map_inf`, `mem_inf`, `comap_inf`, `coe_inf`
`instTop` 📖	CompOp	24 math math: `coe_top`, `toNonUnitalSubsemiring_eq_top`, `prod_top`, `eq_top_iff'`, `comap_top`, `mem_top`, `topEquiv_symm_apply_coe`, `NonUnitalRingHom.eqLocus_same`, `closure_univ`, `center_eq_top`, `topEquiv_apply`, `toAddSubgroup_eq_top`, `NonUnitalRingHom.range_eq_top`, `top_prod`, `top_prod_top`, `toNonUnitalSubsemiring_top`, `NonUnitalRingHom.range_eq_top_of_surjective`, `NonUnitalAlgebra.to_subring_eq_top`, `NonUnitalAlgebra.toNonUnitalSubring_eq_top`, `NonUnitalAlgebra.top_toSubring`, `NonUnitalRingHom.range_eq_map`, `centralizer_eq_top_iff_subset`, `NonUnitalAlgebra.toNonUnitalSubring_top`, `toAddSubgroup_top`
`map` 📖	CompOp	18 math math: `map_inf`, `NonUnitalRingHom.map_closure`, `map_equiv_eq_comap_symm`, `map_iSup`, `map_map`, `map_sup`, `map_le_iff_le_comap`, `mem_map`, `map_bot`, `comap_equiv_eq_map_symm`, `coe_equivMapOfInjective_apply`, `mem_map_equiv`, `map_id`, `coe_map`, `gc_map_comap`, `NonUnitalRingHom.range_eq_map`, `NonUnitalRingHom.map_range`, `map_iInf`
`prod` 📖	CompOp	8 math math: `prod_top`, `top_prod`, `prod_mono_left`, `top_prod_top`, `prod_mono`, `mem_prod`, `prod_mono_right`, `coe_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` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubring` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `center.instNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubring` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `center.instNonUnitalCommRing` `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` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `NonUnitalSubring` `instSetLike` `center` `MulOpposite.instNonUnitalNonAssocRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `center.instNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `RingEquiv` `MulOpposite` `NonUnitalSubring` `MulOpposite.instNonUnitalNonAssocRing` `instSetLike` `center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `center.instNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_eq_top` 📖	mathematical	—	`center` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Top.top` `NonUnitalSubring` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`center_le_centralizer` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.center_subset_centralizer`
`center_toNonUnitalSubsemiring` 📖	mathematical	—	`toNonUnitalSubsemiring` `center` `NonUnitalSubsemiring.center` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.centralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.centralizer_subset`
`centralizer_toNonUnitalSubsemiring` 📖	mathematical	—	`toNonUnitalSubsemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `centralizer` `NonUnitalSubsemiring.centralizer` `NonUnitalRing.toNonUnitalSemiring`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`SetLike.ext'` `Set.centralizer_univ`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `NonUnitalSubring` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `NonUnitalSubring` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `NonUnitalSubring` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	`closure`	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `NonUnitalSubring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ZeroMemClass.zero_mem` `NonUnitalSubring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass` `closure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `SetLike.instMembership`	—	—	`subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ZeroMemClass.zero_mem` `NonUnitalSubring` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass` `closure` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass` `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` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass` `NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `closure_induction`
`closure_le` 📖	mathematical	—	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_centralizer_centralizer`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_preimage_le` 📖	mathematical	—	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set.preimage` `DFunLike.coe` `comap`	—	`closure_le` `SetLike.mem_coe` `mem_comap` `subset_closure`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `iSup` `NonUnitalSubring` `Set` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `GaloisInsertion.gc`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `NonUnitalSubring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `NonUnitalSubring` `instTop`	—	`closure_eq` `coe_top`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`NonUnitalRingHom.coe_range` `Set.range_const` `Zero.instNonempty`
`coe_center` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `center` `Set.center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `instSetLike` `centralizer` `Set.centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`coe_comap` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `comap` `Set.preimage` `DFunLike.coe`	—	—
`coe_equivMapOfInjective_apply` 📖	mathematical	`DFunLike.coe`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivMapOfInjective`	—	`instNonUnitalSubringClass`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `NonUnitalSubring` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `mem_iSup_of_directed`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_map` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `map` `Set.image` `DFunLike.coe`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `Prod.instNonUnitalNonAssocRing` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `NonUnitalSubring` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `NonUnitalSubring` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `mem_sSup_of_directedOn`
`coe_top` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	—	`comap` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.comp`	—	`NonUnitalRingHom.instNonUnitalRingHomClass`
`comap_equiv_eq_map_symm` 📖	mathematical	—	`comap` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `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` `NonUnitalSubring` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_inf` 📖	mathematical	—	`comap` `NonUnitalSubring` `instMin`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_top` 📖	mathematical	—	`comap` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `Top.top` `NonUnitalSubring` `instTop`	—	`GaloisConnection.u_top` `NonUnitalRingHom.instNonUnitalRingHomClass` `gc_map_comap`
`eq_top_iff'` 📖	mathematical	—	`Top.top` `NonUnitalSubring` `instTop` `SetLike.instMembership` `instSetLike`	—	`eq_top_iff` `mem_top`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `NonUnitalSubring` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`instIsMulCommutative_closure` 📖	mathematical	—	`IsMulCommutative` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalRing`	—	`isMulCommutative_closure` `setLike_mul_comm`
`isMulCommutative_closure` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`IsMulCommutative` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `closure` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalRing`	—	`closure_le_centralizer_centralizer` `IsMulCommutative.of_setLike_mul_comm` `NonUnitalSubsemiringClass.mulMemClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `Set.centralizer_centralizer_comm_of_comm`
`list_sum_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`list_sum_mem` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`map_bot` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `Bot.bot` `NonUnitalSubring` `instBot`	—	`GaloisConnection.l_bot` `NonUnitalRingHom.instNonUnitalRingHomClass` `gc_map_comap`
`map_equiv_eq_comap_symm` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `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` `NonUnitalSubring` `instInfSet`	—	`SetLike.coe_injective` `coe_iInf` `Set.InjOn.image_iInter_eq` `Set.injOn_of_injective`
`map_iSup` 📖	mathematical	—	`map` `iSup` `NonUnitalSubring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_id` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.id`	—	`SetLike.coe_injective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Set.image_id`
`map_inf` 📖	mathematical	`DFunLike.coe`	`map` `NonUnitalSubring` `instMin`	—	`SetLike.coe_injective` `Set.image_inter`
`map_le_iff_le_comap` 📖	mathematical	—	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.comp`	—	`SetLike.coe_injective` `NonUnitalRingHom.instNonUnitalRingHomClass` `Set.image_image`
`map_sup` 📖	mathematical	—	`map` `NonUnitalSubring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`mem_bot` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`coe_bot` `Set.mem_singleton_iff`
`mem_center_iff` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`Subsemigroup.mem_center_iff`
`mem_centralizer_iff` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `centralizer` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`mem_closure` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `closure` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike` `AddSubgroup.closure` `SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `Subsemigroup.closure`	—	`closure_induction` `AddSubgroup.subset_closure` `Subsemigroup.subset_closure` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `AddSubgroup.closure_induction₂` `MulMemClass.mul_mem` `Subsemigroup.instMulMemClass` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `neg_mul` `mul_neg` `AddSubgroup.closure_induction` `Subsemigroup.closure_induction` `subset_closure` `NonUnitalSubsemiringClass.mulMemClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNegMemClass`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe`	—	—
`mem_iInf` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup_of_directed` 📖	mathematical	`Directed` `NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`Subsemigroup.coe_iSup_of_directed` `AddSubgroup.coe_iSup_of_directed` `iSup_le` `Set.mem_iUnion` `le_iSup`
`mem_inf` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_map` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe`	—	`Set.mem_image`
`mem_map_equiv` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `map` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `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`	—	`Set.mem_image_equiv`
`mem_prod` 📖	mathematical	—	`NonUnitalSubring` `Prod.instNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `prod`	—	—
`mem_sInf` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `NonUnitalSubring` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NonUnitalSubring` `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	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`multiset_sum_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`multiset_sum_mem` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`notMem_of_notMem_closure` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`prod_mono` 📖	mathematical	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NonUnitalSubring` `Prod.instNonUnitalNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	—	`Monotone` `NonUnitalSubring` `Prod.instNonUnitalNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_mono_right` 📖	mathematical	—	`Monotone` `NonUnitalSubring` `Prod.instNonUnitalNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `prod`	—	`prod_mono` `le_refl`
`prod_top` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubring` `instTop` `comap` `NonUnitalRingHom` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Prod.instNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.fst`	—	`ext` `NonUnitalRingHom.instNonUnitalRingHomClass`
`range_fst` 📖	mathematical	—	`NonUnitalRingHom.srange` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.fst` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop`	—	`NonUnitalSubsemiring.range_fst`
`range_snd` 📖	mathematical	—	`NonUnitalRingHom.srange` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.snd` `Top.top` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instTop`	—	`NonUnitalSubsemiring.range_snd`
`range_subtype` 📖	mathematical	—	`NonUnitalRingHom.range` `NonUnitalSubring` `SetLike.instMembership` `instSetLike` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass` `NonUnitalSubringClass.subtype`	—	`SetLike.coe_injective` `instNonUnitalSubringClass` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.coe_srange` `Subtype.range_coe`
`sInf_toAddSubgroup` 📖	mathematical	—	`toAddSubgroup` `InfSet.sInf` `NonUnitalSubring` `instInfSet` `iInf` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instInfSet` `Set` `Set.instMembership`	—	`mk'_toAddSubgroup`
`sInf_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `InfSet.sInf` `NonUnitalSubring` `instInfSet` `iInf` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instInfSet` `Set` `Set.instMembership`	—	`mk'_toSubsemigroup`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `NonUnitalSubring` `instSetLike` `closure`	—	`mem_closure`
`sum_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`sum_mem` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`toAddSubgroup_eq_top` 📖	mathematical	—	`toAddSubgroup` `Top.top` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instTop` `NonUnitalSubring` `instTop`	—	—
`toAddSubgroup_top` 📖	mathematical	—	`toAddSubgroup` `Top.top` `NonUnitalSubring` `instTop` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instTop`	—	—
`toNonUnitalSubsemiring_eq_top` 📖	mathematical	—	`toNonUnitalSubsemiring` `Top.top` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instTop` `NonUnitalSubring` `instTop`	—	—
`toNonUnitalSubsemiring_top` 📖	mathematical	—	`toNonUnitalSubsemiring` `Top.top` `NonUnitalSubring` `instTop` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instTop`	—	—
`topEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `topEquiv` `Subsemigroup` `Subsemigroup.instSetLike` `Subsemigroup.instTop`	—	`instNonUnitalSubringClass`
`topEquiv_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `Top.top` `Subsemigroup.instTop` `DFunLike.coe` `RingEquiv` `NonUnitalSubring` `instSetLike` `instTop` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `topEquiv`	—	`instNonUnitalSubringClass`
`top_prod` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubring` `instTop` `comap` `NonUnitalRingHom` `Prod.instNonUnitalNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Prod.instNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike` `NonUnitalRingHom.instNonUnitalRingHomClass` `NonUnitalRingHom.snd`	—	`ext` `NonUnitalRingHom.instNonUnitalRingHomClass`
`top_prod_top` 📖	mathematical	—	`prod` `Top.top` `NonUnitalSubring` `instTop` `Prod.instNonUnitalNonAssocRing`	—	`NonUnitalRingHom.instNonUnitalRingHomClass` `top_prod` `comap_top`

NonUnitalSubring.center

Definitions

Name	Category	Theorems
`instNonUnitalCommRing` 📖	CompOp	4 math math: `NonUnitalSubring.centerCongr_apply_coe`, `NonUnitalSubring.centerCongr_symm_apply_coe`, `NonUnitalSubring.centerToMulOpposite_symm_apply_coe`, `NonUnitalSubring.centerToMulOpposite_apply_coe`

RingEquiv

Definitions

Name	Category	Theorems
`nonUnitalSubringCongr` 📖	CompOp	—
`ofLeftInverse'` 📖	CompOp	2 math math: `ofLeftInverse'_symm_apply`, `ofLeftInverse'_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLeftInverse'_apply` 📖	mathematical	`DFunLike.coe` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike`	`NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `NonUnitalSubring.instSetLike` `NonUnitalRingHom.range` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubring.toNonUnitalRing` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `ofLeftInverse'` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike`	—	—
`ofLeftInverse'_symm_apply` 📖	mathematical	`DFunLike.coe` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike`	`DFunLike.coe` `RingEquiv` `NonUnitalSubring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `NonUnitalSubring.instSetLike` `NonUnitalRingHom.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubring.toNonUnitalRing` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `ofLeftInverse'`	—	—

---

← Back to Index