NonUnitalSubalgebra

📁 Source: Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Statistics

Metric	Count
Definitions codRestrict, equalizer, fintypeRange, range, rangeRestrict, adjoin, adjoinNonUnitalCommRingOfComm, adjoinNonUnitalCommSemiringOfComm, gi, instCompleteLatticeNonUnitalSubalgebra, instInhabitedNonUnitalSubalgebra, toTop, center, instNonUnitalCommRing, instNonUnitalCommSemiring, centralizer, comap, copy, iSupLift, inclusion, instInhabitedSubtypeMem, instModule, instModule', instPartialOrder, instSetLike, map, ofClass, prod, toNonUnitalCommRing, toNonUnitalCommSemiring, toNonUnitalNonAssocRing, toNonUnitalNonAssocSemiring, toNonUnitalRing, toNonUnitalSemiring, toNonUnitalSubring, toNonUnitalSubring', toNonUnitalSubsemiring, toNonUnitalSubsemiring', toSubmodule, toSubmodule', toSubmoduleEquiv, subtype, toNonUnitalSubalgebra, nonUnitalSubalgebraOfNonUnitalSubring, nonUnitalSubalgebraOfNonUnitalSubsemiring	45
Theorems coe_codRestrict, coe_range, injective_codRestrict, map_adjoin, map_adjoin_singleton, mem_equalizer, mem_range, mem_range_self, range_comp, range_comp_le_range, subsingleton, subtype_comp_codRestrict, adjoin_empty, adjoin_eq, adjoin_eq_span, adjoin_induction, adjoin_induction₂, adjoin_le, adjoin_le_centralizer_centralizer, adjoin_le_iff, adjoin_mono, adjoin_toSubmodule, adjoin_union, adjoin_univ, coe_bot, coe_iInf, coe_inf, coe_sInf, coe_top, comap_top, commute_of_mem_adjoin_of_forall_mem_commute, commute_of_mem_adjoin_self, commute_of_mem_adjoin_singleton_of_commute, eq_top_iff, gc, iInf_toSubmodule, inf_toNonUnitalSubsemiring, inf_toSubmodule, map_bot, map_iInf, map_inf, map_sup, map_top, mem_adjoin_of_mem, mem_bot, mem_iInf, mem_inf, mem_sInf, mem_sup_left, mem_sup_right, mem_top, mul_mem_sup, range_eq_top, range_id, sInf_toNonUnitalSubsemiring, sInf_toSubmodule, self_mem_adjoin_singleton, span_eq_toSubmodule, subset_adjoin, toNonUnitalSubring_eq_top, toNonUnitalSubring_top, toNonUnitalSubsemiring_eq_top, toSubmodule_bot, toSubmodule_eq_top, to_subring_eq_top, top_toNonUnitalSubsemiring, top_toSubmodule, top_toSubring, center_eq_top, center_toNonUnitalSubring, center_toNonUnitalSubsemiring, centralizer_le, centralizer_univ, coe_add, coe_center, coe_centralizer, coe_comap, coe_copy, coe_eq_zero, coe_iSup_of_directed, coe_inclusion, coe_map, coe_mul, coe_neg, coe_prod, coe_smul, coe_sub, coe_toNonUnitalSubring, coe_toNonUnitalSubsemiring, coe_toSubmodule, coe_zero, copy_eq, ext, ext_iff, gc_map_comap, iSupLift_comp_inclusion, iSupLift_inclusion, iSupLift_mk, iSupLift_of_mem, inclusion_inclusion, inclusion_injective, inclusion_mk, inclusion_right, inclusion_self, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul, instIsScalarTower', instIsScalarTowerSubtypeMem, instIsTorsionFree, instNonUnitalSubringClass, instNonUnitalSubsemiringClass, instSMulCommClass, instSMulCommClass', instSMulMemClass, map_id, map_injective, map_le, map_map, map_mono, map_toNonUnitalSubsemiring, map_toSubmodule, mem_carrier, mem_center_iff, mem_centralizer_iff, mem_comap, mem_map, mem_prod, mem_toNonUnitalSubring, mem_toNonUnitalSubsemiring, mem_toSubmodule, noZeroDivisors, ofClass_carrier, prod_inf_prod, prod_mono, prod_toSubmodule, prod_top, range_val, smul_mem', subsingleton_of_subsingleton, toNonUnitalSubring_inj, toNonUnitalSubring_injective, toNonUnitalSubsemiring_inj, toNonUnitalSubsemiring_injective, toNonUnitalSubsemiring_subtype, toSubmodule_inj, toSubmodule_injective, toSubmodule_toNonUnitalSubalgebra, toSubring_subtype, coe_subtype, subtype_apply, subtype_injective, smul_mem_center, smul_mem_centralizer, coe_toNonUnitalSubalgebra, mem_toNonUnitalSubalgebra, toNonUnitalSubalgebra_mk, toNonUnitalSubalgebra_toSubmodule, mem_nonUnitalSubalgebraOfNonUnitalSubring, mem_nonUnitalSubalgebraOfNonUnitalSubsemiring	158
Total	203

NonUnitalAlgHom

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	3 math math: injective_codRestrict, coe_codRestrict, subtype_comp_codRestrict
equalizer 📖	CompOp	1 math math: mem_equalizer
fintypeRange 📖	CompOp	—
range 📖	CompOp	11 math math: range_comp_le_range, NonUnitalAlgebra.range_id, mem_range, mem_range_self, Unitization.lift_range, coe_range, NonUnitalAlgebra.map_top, range_comp, Unitization.lift_range_le, NonUnitalAlgebra.range_eq_top, NonUnitalSubalgebra.range_val
rangeRestrict 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_codRestrict 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike DFunLike.coe	NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubalgebra.toNonUnitalNonAssocSemiring NonUnitalSubalgebra.instModule instFunLike_1 codRestrict	—	—
coe_range 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike range Set.range DFunLike.coe	—	Set.ext SetLike.mem_coe mem_range Set.mem_range
injective_codRestrict 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike DFunLike.coe	NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubalgebra.toNonUnitalNonAssocSemiring NonUnitalSubalgebra.instModule instFunLike_1 codRestrict	—	—
map_adjoin 📖	mathematical	—	NonUnitalSubalgebra.map NonUnitalAlgebra.adjoin Set.image DFunLike.coe	—	GaloisConnection.l_comm_of_u_comm Set.image_preimage NonUnitalSubalgebra.gc_map_comap GaloisInsertion.gc
map_adjoin_singleton 📖	mathematical	—	NonUnitalSubalgebra.map NonUnitalAlgebra.adjoin Set Set.instSingletonSet DFunLike.coe	—	map_adjoin NonUnitalAlgebra.adjoin.congr_simp Set.image_singleton
mem_equalizer 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike equalizer DFunLike.coe	—	—
mem_range 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike range DFunLike.coe	—	NonUnitalRingHom.mem_srange NonUnitalRingHom.instNonUnitalRingHomClass
mem_range_self 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike range DFunLike.coe	—	mem_range
range_comp 📖	mathematical	—	range NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 instNonUnitalAlgSemiHomClass comp MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId NonUnitalSubalgebra.map	—	SetLike.coe_injective instNonUnitalAlgSemiHomClass MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId Set.range_comp
range_comp_le_range 📖	mathematical	—	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder range NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 instNonUnitalAlgSemiHomClass comp MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	SetLike.coe_mono instIsConcreteLE instNonUnitalAlgSemiHomClass MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId Set.range_comp_subset_range
subsingleton 📖	mathematical	—	NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid	—	ext NonUnitalAlgebra.mem_top map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass NonUnitalAlgebra.mem_bot
subtype_comp_codRestrict 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike DFunLike.coe	comp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring NonUnitalSubalgebra.instNonUnitalSubsemiringClass SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instSMulMemClass NonUnitalSubalgebraClass.subtype codRestrict MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId NonUnitalAlgHomClass.toNonUnitalAlgHom	—	NonUnitalSubalgebra.instNonUnitalSubsemiringClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instSMulMemClass MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId

NonUnitalAlgebra

Definitions

Name	Category	Theorems
adjoin 📖	CompOp	22 math math: adjoin_le_algebra_adjoin, gc, adjoin_le, adjoin_le_centralizer_centralizer, self_mem_adjoin_singleton, subset_adjoin, NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra, NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin, NonUnitalAlgHom.map_adjoin, adjoin_le_iff, adjoin_univ, Algebra.adjoin_nonUnitalSubalgebra, NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, adjoin_empty, NonUnitalAlgHom.map_adjoin_singleton, adjoin_toSubmodule, adjoin_eq, adjoin_union, mem_adjoin_of_mem, adjoin_mono, adjoin_eq_span, NonUnitalSubalgebra.star_adjoin_comm
adjoinNonUnitalCommRingOfComm 📖	CompOp	—
adjoinNonUnitalCommSemiringOfComm 📖	CompOp	—
gi 📖	CompOp	—
instCompleteLatticeNonUnitalSubalgebra 📖	CompOp	52 math math: NonUnitalSubalgebra.coe_starClosure, NonUnitalSubalgebra.center_eq_top, coe_bot, mem_sup_left, coe_inf, sInf_toNonUnitalSubsemiring, NonUnitalSubalgebra.prod_inf_prod, mem_sup_right, NonUnitalSubalgebra.prod_top, mem_inf, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, range_id, mem_iInf, mul_mem_sup, toSubmodule_bot, top_toNonUnitalSubsemiring, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, NonUnitalSubalgebra.coe_iSup_of_directed, map_sup, eq_top_iff, coe_iInf, mem_top, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, adjoin_univ, map_iInf, toSubmodule_eq_top, adjoin_empty, coe_top, map_top, to_subring_eq_top, toNonUnitalSubring_eq_top, inf_toSubmodule, mem_sInf, comap_top, map_bot, coe_sInf, range_eq_top, top_toSubring, mem_bot, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, top_toSubmodule, NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, sInf_toSubmodule, toNonUnitalSubring_top, adjoin_union, inf_toNonUnitalSubsemiring, toNonUnitalSubsemiring_eq_top, NonUnitalSubalgebra.mem_starClosure, NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, map_inf, iInf_toSubmodule, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra
instInhabitedNonUnitalSubalgebra 📖	CompOp	—
toTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_empty 📖	mathematical	—	adjoin Set Set.instEmptyCollection Bot.bot NonUnitalSubalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot gc
adjoin_eq 📖	mathematical	—	adjoin SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike	—	le_antisymm adjoin_le le_rfl subset_adjoin
adjoin_eq_span 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule adjoin Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.coe Subsemigroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Subsemigroup.instSetLike Subsemigroup.closure	—	le_antisymm adjoin_induction Submodule.subset_span Subsemigroup.subset_closure AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.span_induction₂ MulMemClass.mul_mem Subsemigroup.instMulMemClass MulZeroClass.zero_mul MulZeroClass.mul_zero add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass smul_mul_assoc Submodule.smul_mem mul_smul_comm Submodule.span_le Subsemigroup.closure_le subset_adjoin
adjoin_induction 📖	—	subset_adjoin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMemClass.add_mem NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass adjoin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Distrib.toMul MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction SMulMemClass.smul_mem NonUnitalSubalgebra.instSMulMemClass SetLike.instMembership	—	—	subset_adjoin AddMemClass.add_mem AddSubmonoidClass.toAddMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass SMulMemClass.smul_mem NonUnitalSubalgebra.instSMulMemClass adjoin_le
adjoin_induction₂ 📖	—	subset_adjoin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ZeroMemClass.zero_mem NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass adjoin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Distrib.toMul MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction SMulMemClass.smul_mem NonUnitalSubalgebra.instSMulMemClass SetLike.instMembership	—	—	subset_adjoin ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass SMulMemClass.smul_mem NonUnitalSubalgebra.instSMulMemClass adjoin_induction
adjoin_le 📖	mathematical	Set Set.instHasSubset SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike	Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder adjoin	—	GaloisConnection.l_le gc
adjoin_le_centralizer_centralizer 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder adjoin NonUnitalSubalgebra.centralizer SetLike.coe NonUnitalSubalgebra.instSetLike	—	adjoin_le Set.subset_centralizer_centralizer
adjoin_le_iff 📖	mathematical	—	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder adjoin Set Set.instHasSubset SetLike.coe NonUnitalSubalgebra.instSetLike	—	gc
adjoin_mono 📖	mathematical	Set Set.instHasSubset	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder adjoin	—	GaloisConnection.monotone_l gc
adjoin_toSubmodule 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule adjoin Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.coe NonUnitalSubsemiring NonUnitalSubsemiring.instSetLike NonUnitalSubsemiring.closure	—	—
adjoin_union 📖	mathematical	—	adjoin Set Set.instUnion NonUnitalSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	GaloisConnection.l_sup gc
adjoin_univ 📖	mathematical	—	adjoin Set.univ Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff subset_adjoin
coe_bot 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
coe_iInf 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Set.iInter	—	coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.iInter_iInter_eq'
coe_inf 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Set Set.instInter	—	—
coe_sInf 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Set.iInter Set Set.instMembership	—	sInf_image
coe_top 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
comap_top 📖	mathematical	—	NonUnitalSubalgebra.comap NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	NonUnitalAlgHom.instNonUnitalAlgSemiHomClass eq_top_iff mem_top
commute_of_mem_adjoin_of_forall_mem_commute 📖	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubalgebra.instSetLike adjoin Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	Commute.symm_iff adjoin_le_centralizer_centralizer
commute_of_mem_adjoin_self 📖	mathematical	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubalgebra.instSetLike adjoin Set Set.instSingletonSet	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	commute_of_mem_adjoin_singleton_of_commute
commute_of_mem_adjoin_singleton_of_commute 📖	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubalgebra.instSetLike adjoin Set Set.instSingletonSet Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	commute_of_mem_adjoin_of_forall_mem_commute
eq_top_iff 📖	mathematical	—	Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder SetLike.instMembership NonUnitalSubalgebra.instSetLike	—	mem_top NonUnitalSubalgebra.ext
gc 📖	mathematical	—	GaloisConnection Set NonUnitalSubalgebra PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra NonUnitalSubalgebra.instPartialOrder adjoin SetLike.coe NonUnitalSubalgebra.instSetLike	—	HasSubset.Subset.trans Set.instIsTransSubset NonUnitalSubsemiring.subset_closure Submodule.subset_span Submodule.span_le NonUnitalSubsemiring.closure_le
iInf_toSubmodule 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule iInf NonUnitalSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instInfSet	—	SetLike.coe_injective coe_iInf Submodule.coe_iInf
inf_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubsemiring NonUnitalSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra NonUnitalSubsemiring NonUnitalSubsemiring.instMin	—	—
inf_toSubmodule 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule NonUnitalSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instMin	—	—
map_bot 📖	mathematical	—	NonUnitalSubalgebra.map NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Bot.bot NonUnitalSubalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	SetLike.coe_injective NonUnitalAlgHom.instNonUnitalAlgSemiHomClass coe_bot Set.image_singleton map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass
map_iInf 📖	mathematical	DFunLike.coe	NonUnitalSubalgebra.map iInf NonUnitalSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	SetLike.coe_injective coe_iInf Set.InjOn.image_iInter_eq Set.injOn_of_injective
map_inf 📖	mathematical	DFunLike.coe	NonUnitalSubalgebra.map NonUnitalSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	SetLike.coe_injective Set.image_inter
map_sup 📖	mathematical	—	NonUnitalSubalgebra.map NonUnitalSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	GaloisConnection.l_sup NonUnitalSubalgebra.gc_map_comap
map_top 📖	mathematical	—	NonUnitalSubalgebra.map NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalAlgHom.range	—	SetLike.coe_injective NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Set.image_univ
mem_adjoin_of_mem 📖	mathematical	Set Set.instMembership	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike adjoin	—	subset_adjoin
mem_bot 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	NonUnitalSubsemiring.closure_empty NonUnitalSubsemiring.coe_bot Submodule.span_zero_singleton Submodule.mem_bot
mem_iInf 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	—
mem_inf 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	—
mem_sInf 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	coe_sInf
mem_sup_left 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	SetLike.le_def instIsConcreteLE le_sup_left
mem_sup_right 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra	—	SetLike.le_def instIsConcreteLE le_sup_right
mem_top 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_univ
mul_mem_sup 📖	mathematical	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass mem_sup_left mem_sup_right
range_eq_top 📖	mathematical	—	NonUnitalAlgHom.range NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe	—	eq_top_iff NonUnitalAlgHom.instNonUnitalAlgSemiHomClass
range_id 📖	mathematical	—	NonUnitalAlgHom.range NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalAlgHom.id Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Set.range_id
sInf_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubsemiring InfSet.sInf NonUnitalSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra NonUnitalSubsemiring NonUnitalSubsemiring.instInfSet Set.image	—	SetLike.coe_injective coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
sInf_toSubmodule 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule InfSet.sInf NonUnitalSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalSubalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instInfSet Set.image	—	SetLike.coe_injective coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
self_mem_adjoin_singleton 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike adjoin Set Set.instSingletonSet	—	subset_adjoin Set.mem_singleton
span_eq_toSubmodule 📖	mathematical	—	Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike NonUnitalSubalgebra.toSubmodule	—	Submodule.coe_span_eq_self NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalSubalgebra.instNonUnitalSubsemiringClass NonUnitalSubalgebra.instSMulMemClass
subset_adjoin 📖	mathematical	—	Set Set.instHasSubset SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike adjoin	—	HasSubset.Subset.trans Set.instIsTransSubset NonUnitalSubsemiring.subset_closure Submodule.subset_span
toNonUnitalSubring_eq_top 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule CommRing.toCommSemiring Ring.toSemiring Top.top NonUnitalSubring NonUnitalSubring.instTop NonUnitalSubalgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra IsScalarTower.right Algebra.to_smulCommClass BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsScalarTower.right Algebra.to_smulCommClass
toNonUnitalSubring_top 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubring Top.top NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalSubring NonUnitalSubring.instTop	—	—
toNonUnitalSubsemiring_eq_top 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubsemiring Top.top NonUnitalSubsemiring NonUnitalSubsemiring.instTop NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
toSubmodule_bot 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule Bot.bot NonUnitalSubalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instBot	—	Submodule.ext
toSubmodule_eq_top 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule Top.top Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instTop NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	NonUnitalSubalgebra.smul_mem'
to_subring_eq_top 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule CommRing.toCommSemiring Ring.toSemiring Top.top NonUnitalSubring NonUnitalSubring.instTop NonUnitalSubalgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra IsScalarTower.right Algebra.to_smulCommClass BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	toNonUnitalSubring_eq_top
top_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubsemiring Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalSubsemiring NonUnitalSubsemiring.instTop	—	—
top_toSubmodule 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.instTop	—	—
top_toSubring 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalSubring Top.top NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalSubring NonUnitalSubring.instTop	—	toNonUnitalSubring_top

NonUnitalSubalgebra

Definitions

Name	Category	Theorems
center 📖	CompOp	7 math math: center_eq_top, NonUnitalStarSubalgebra.center_toNonUnitalSubalgebra, centralizer_univ, mem_center_iff, center_toNonUnitalSubsemiring, coe_center, center_toNonUnitalSubring
centralizer 📖	CompOp	8 math math: NonUnitalAlgebra.adjoin_le_centralizer_centralizer, centralizer_univ, mem_centralizer_iff, centralizer_le, topologicalClosure_adjoin_le_centralizer_centralizer, coe_centralizer, NonUnitalAlgebra.elemental.le_centralizer_centralizer, NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra
comap 📖	CompOp	5 math math: map_le, mem_comap, coe_comap, gc_map_comap, NonUnitalAlgebra.comap_top
copy 📖	CompOp	2 math math: copy_eq, coe_copy
iSupLift 📖	CompOp	4 math math: iSupLift_of_mem, iSupLift_comp_inclusion, iSupLift_mk, iSupLift_inclusion
inclusion 📖	CompOp	6 math math: inclusion_mk, inclusion_right, inclusion_self, inclusion_injective, inclusion_inclusion, coe_inclusion
instInhabitedSubtypeMem 📖	CompOp	—
instModule 📖	CompOp	14 math math: instIsScalarTower', inclusion_mk, inclusion_right, inclusion_self, inclusion_injective, NonUnitalAlgHom.injective_codRestrict, instSMulCommClass, inclusion_inclusion, instSMulCommClass', instIsTorsionFree, instIsScalarTowerSubtypeMem, coe_inclusion, NonUnitalAlgHom.coe_codRestrict, range_val
instModule' 📖	CompOp	2 math math: instIsScalarTower', instSMulCommClass'
instPartialOrder 📖	CompOp	23 math math: NonUnitalAlgebra.adjoin_le_algebra_adjoin, NonUnitalAlgebra.gc, NonUnitalAlgebra.adjoin_le, NonUnitalAlgHom.range_comp_le_range, topologicalClosure_map_le, NonUnitalAlgebra.adjoin_le_centralizer_centralizer, starClosure_le_iff, inclusion_self, NonUnitalAlgebra.adjoin_le_iff, starClosure_mono, map_le, le_topologicalClosure, NonUnitalAlgebra.elemental.le_of_mem, centralizer_le, gc_map_comap, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff, topologicalClosure_adjoin_le_centralizer_centralizer, map_topologicalClosure_le, star_mono, NonUnitalAlgebra.elemental.le_centralizer_centralizer, Unitization.lift_range_le, NonUnitalAlgebra.elemental.le_iff_mem, NonUnitalAlgebra.adjoin_mono
instSetLike 📖	CompOp	94 math math: coe_starClosure, NonUnitalAlgebra.gc, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul, instIsScalarTower', NonUnitalAlgebra.coe_bot, NonUnitalAlgebra.span_eq_toSubmodule, NonUnitalAlgebra.coe_inf, NonUnitalAlgebra.elemental.isClosedEmbedding_coe, NonUnitalAlgebra.adjoin_le_centralizer_centralizer, coe_toNonUnitalSubring, NonUnitalAlgebra.self_mem_adjoin_singleton, ext_iff, instNonUnitalSubsemiringClass, NonUnitalAlgebra.mem_inf, coe_toNonUnitalSubsemiring, inclusion_self, mem_toNonUnitalSubsemiring, NonUnitalAlgebra.subset_adjoin, NonUnitalAlgHom.mem_range, NonUnitalAlgebra.mem_iInf, mem_map, NonUnitalAlgHom.mem_range_self, mem_star_iff, inclusion_injective, NonUnitalAlgebra.adjoin_le_iff, Algebra.adjoin_nonUnitalSubalgebra_eq_span, noZeroDivisors, coe_sub, toSubring_subtype, coe_zero, NonUnitalAlgebra.elemental.isClosed, instSMulCommClass, mem_comap, inclusion_inclusion, coe_iSup_of_directed, NonUnitalAlgebra.eq_top_iff, starClosure_eq_adjoin, mem_centralizer_iff, coe_comap, NonUnitalAlgebra.coe_iInf, Unitization.lift_range, NonUnitalAlgebra.mem_top, NonUnitalAlgHom.coe_range, mem_center_iff, coe_map, NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra, coe_star, instSMulMemClass, Algebra.adjoin_nonUnitalSubalgebra, ofClass_carrier, topologicalClosure_adjoin_le_centralizer_centralizer, instIsTopologicalRing, instSMulCommClass', isClosed_topologicalClosure, mem_carrier, coe_centralizer, coe_center, toSubmodule_toNonUnitalSubalgebra, coe_prod, NonUnitalAlgebra.elemental.le_centralizer_centralizer, NonUnitalAlgebra.coe_top, instIsTorsionFree, coe_smul, NonUnitalAlgebra.mem_sInf, NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra, instIsTopologicalSemiring, toNonUnitalSubsemiring_subtype, coe_neg, instNonUnitalSubringClass, Submodule.coe_toNonUnitalSubalgebra, instIsScalarTowerSubtypeMem, NonUnitalAlgebra.elemental.le_iff_mem, NonUnitalAlgebra.coe_sInf, coe_inclusion, mem_nonUnitalSubalgebraOfNonUnitalSubsemiring, NonUnitalAlgebra.elemental.self_mem, mem_toSubmodule, NonUnitalAlgebra.mem_bot, NonUnitalAlgebra.adjoin_eq, mem_nonUnitalSubalgebraOfNonUnitalSubring, coe_mul, NonUnitalAlgHom.mem_equalizer, coe_toSubmodule, NonUnitalAlgebra.mem_adjoin_of_mem, mem_toNonUnitalSubring, coe_eq_zero, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, mem_prod, mem_starClosure, Subalgebra.one_mem_toNonUnitalSubalgebra, coe_add, range_val, Submodule.mem_toNonUnitalSubalgebra, star_mem_star_iff
map 📖	CompOp	22 math math: topologicalClosure_map_le, topologicalClosure_map, mem_map, NonUnitalAlgHom.map_adjoin, map_le, map_mono, NonUnitalAlgebra.map_sup, map_toNonUnitalSubsemiring, gc_map_comap, coe_map, NonUnitalAlgebra.map_iInf, map_topologicalClosure_le, NonUnitalAlgHom.map_adjoin_singleton, NonUnitalAlgebra.map_top, NonUnitalAlgHom.range_comp, NonUnitalAlgebra.map_bot, map_injective, map_map, NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra, map_id, NonUnitalAlgebra.map_inf, map_toSubmodule
ofClass 📖	CompOp	1 math math: ofClass_carrier
prod 📖	CompOp	7 math math: NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra, prod_inf_prod, prod_top, coe_prod, prod_toSubmodule, mem_prod, prod_mono
toNonUnitalCommRing 📖	CompOp	—
toNonUnitalCommSemiring 📖	CompOp	—
toNonUnitalNonAssocRing 📖	CompOp	1 math math: instIsTopologicalRing
toNonUnitalNonAssocSemiring 📖	CompOp	17 math math: instIsScalarTower', inclusion_mk, inclusion_right, inclusion_self, inclusion_injective, noZeroDivisors, NonUnitalAlgHom.injective_codRestrict, instSMulCommClass, inclusion_inclusion, instSMulCommClass', instIsTorsionFree, instIsTopologicalSemiring, instIsScalarTowerSubtypeMem, coe_inclusion, coe_mul, NonUnitalAlgHom.coe_codRestrict, coe_add
toNonUnitalRing 📖	CompOp	—
toNonUnitalSemiring 📖	CompOp	—
toNonUnitalSubring 📖	CompOp	9 math math: coe_toNonUnitalSubring, toNonUnitalSubring_inj, toNonUnitalSubring_injective, NonUnitalAlgebra.to_subring_eq_top, NonUnitalAlgebra.toNonUnitalSubring_eq_top, center_toNonUnitalSubring, NonUnitalAlgebra.top_toSubring, NonUnitalAlgebra.toNonUnitalSubring_top, mem_toNonUnitalSubring
toNonUnitalSubring' 📖	CompOp	—
toNonUnitalSubsemiring 📖	CompOp	12 math math: NonUnitalStarSubalgebra.mem_carrier, NonUnitalAlgebra.sInf_toNonUnitalSubsemiring, coe_toNonUnitalSubsemiring, mem_toNonUnitalSubsemiring, NonUnitalAlgebra.top_toNonUnitalSubsemiring, toNonUnitalSubsemiring_inj, map_toNonUnitalSubsemiring, center_toNonUnitalSubsemiring, mem_carrier, toNonUnitalSubsemiring_injective, NonUnitalAlgebra.inf_toNonUnitalSubsemiring, NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top
toNonUnitalSubsemiring' 📖	CompOp	—
toSubmodule 📖	CompOp	21 math math: NonUnitalAlgebra.span_eq_toSubmodule, toSubmodule_injective, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, NonUnitalAlgebra.toSubmodule_bot, Algebra.adjoin_nonUnitalSubalgebra_eq_span, NonUnitalStarAlgebra.adjoin_eq_span, toSubmodule_inj, NonUnitalAlgebra.toSubmodule_eq_top, toSubmodule_toNonUnitalSubalgebra, NonUnitalAlgebra.inf_toSubmodule, NonUnitalStarAlgebra.span_eq_toSubmodule, Submodule.toNonUnitalSubalgebra_toSubmodule, NonUnitalAlgebra.adjoin_toSubmodule, mem_toSubmodule, NonUnitalAlgebra.top_toSubmodule, prod_toSubmodule, NonUnitalAlgebra.sInf_toSubmodule, coe_toSubmodule, NonUnitalAlgebra.iInf_toSubmodule, map_toSubmodule, NonUnitalAlgebra.adjoin_eq_span
toSubmodule' 📖	CompOp	—
toSubmoduleEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_top 📖	mathematical	—	center NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective Set.center_eq_univ
center_toNonUnitalSubring 📖	mathematical	—	toNonUnitalSubring center CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalSubring.center	—	—
center_toNonUnitalSubsemiring 📖	mathematical	—	toNonUnitalSubsemiring center NonUnitalSubsemiring.center	—	—
centralizer_le 📖	mathematical	Set Set.instHasSubset	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	Set.centralizer_subset
centralizer_univ 📖	mathematical	—	centralizer Set.univ center NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	SetLike.ext' Set.centralizer_univ
coe_add 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib toNonUnitalNonAssocSemiring	—	—
coe_center 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra instSetLike center Set.center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_centralizer 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring instSetLike centralizer Set.centralizer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_comap 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra instSetLike comap Set.preimage DFunLike.coe	—	—
coe_copy 📖	mathematical	SetLike.coe NonUnitalSubalgebra instSetLike	copy	—	—
coe_eq_zero 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ZeroMemClass.zero AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass	—	ZeroMemClass.coe_eq_zero AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass
coe_iSup_of_directed 📖	mathematical	Directed NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.coe instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Set.iUnion	—	NonUnitalSubsemiring.coe_iSup_of_directed Set.mem_iUnion smul_mem' le_antisymm iSup_le le_iSup Set.iUnion_subset
coe_inclusion 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule NonUnitalAlgHom.instFunLike_1 inclusion	—	—
coe_map 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra instSetLike map Set.image DFunLike.coe	—	—
coe_mul 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib toNonUnitalNonAssocSemiring	—	—
coe_neg 📖	mathematical	—	NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership instSetLike NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClass	—	NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClass
coe_prod 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid instSetLike prod SProd.sprod Set Set.instSProd	—	—
coe_smul 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike SetLike.smul' MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction instSMulMemClass	—	instSMulMemClass
coe_sub 📖	mathematical	—	NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership instSetLike AddSubgroupClass.sub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NonUnitalSubringClass.addSubgroupClass instNonUnitalSubringClass SubNegMonoid.toSub	—	NonUnitalSubringClass.addSubgroupClass instNonUnitalSubringClass
coe_toNonUnitalSubring 📖	mathematical	—	SetLike.coe NonUnitalSubring NonUnitalSubring.instSetLike toNonUnitalSubring NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	—
coe_toNonUnitalSubsemiring 📖	mathematical	—	SetLike.coe NonUnitalSubsemiring NonUnitalSubsemiring.instSetLike toNonUnitalSubsemiring NonUnitalSubalgebra instSetLike	—	—
coe_toSubmodule 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.setLike toSubmodule NonUnitalSubalgebra instSetLike	—	—
coe_zero 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass	—	AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass
copy_eq 📖	mathematical	SetLike.coe NonUnitalSubalgebra instSetLike	copy	—	SetLike.coe_injective
ext 📖	—	NonUnitalSubalgebra SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike	—	ext
gc_map_comap 📖	mathematical	—	GaloisConnection NonUnitalSubalgebra PartialOrder.toPreorder instPartialOrder map comap	—	map_le
iSupLift_comp_inclusion 📖	mathematical	Directed NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.comp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule inclusion MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	iSupLift	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId NonUnitalAlgHom.ext iSupLift_inclusion
iSupLift_inclusion 📖	mathematical	Directed NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.comp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule inclusion MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	DFunLike.coe NonUnitalAlgHom NonUnitalAlgHom.instFunLike_1 iSupLift	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId Set.iUnionLift_inclusion
iSupLift_mk 📖	mathematical	Directed NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.comp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule inclusion MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	DFunLike.coe NonUnitalAlgHom NonUnitalAlgHom.instFunLike_1 iSupLift	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId
iSupLift_of_mem 📖	mathematical	Directed NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.comp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule inclusion MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	DFunLike.coe NonUnitalAlgHom NonUnitalAlgHom.instFunLike_1 iSupLift	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId Set.iUnionLift_of_mem
inclusion_inclusion 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule NonUnitalAlgHom.instFunLike_1 inclusion le_trans	—	le_trans
inclusion_injective 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule NonUnitalAlgHom.instFunLike_1 inclusion	—	—
inclusion_mk 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule NonUnitalAlgHom.instFunLike_1 inclusion	—	—
inclusion_right 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule NonUnitalAlgHom.instFunLike_1 inclusion	—	—
inclusion_self 📖	mathematical	—	inclusion le_refl NonUnitalSubalgebra PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.id SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instModule	—	le_refl
instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul 📖	mathematical	—	CanLift Set NonUnitalSubalgebra SetLike.coe instSetLike Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
instIsScalarTower' 📖	mathematical	—	IsScalarTower NonUnitalSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid toNonUnitalNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule instModule'	—	Submodule.isScalarTower
instIsScalarTowerSubtypeMem 📖	mathematical	—	IsScalarTower NonUnitalSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid toNonUnitalNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule instDistribSMul	—	smul_assoc
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree NonUnitalSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toNonUnitalNonAssocSemiring instModule	—	Submodule.instIsTorsionFree
instNonUnitalSubringClass 📖	mathematical	—	NonUnitalSubringClass NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	instNonUnitalSubsemiringClass SMulMemClass.smul_mem instSMulMemClass neg_one_smul
instNonUnitalSubsemiringClass 📖	mathematical	—	NonUnitalSubsemiringClass NonUnitalSubalgebra instSetLike	—	AddSubsemigroup.add_mem' AddSubmonoid.zero_mem' NonUnitalSubsemiring.mul_mem'
instSMulCommClass 📖	mathematical	—	SMulCommClass NonUnitalSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid toNonUnitalNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule instDistribSMul	—	SMulCommClass.smul_comm
instSMulCommClass' 📖	mathematical	—	SMulCommClass NonUnitalSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid toNonUnitalNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule' CommSemiring.toSemiring instModule	—	SMulCommClass.smul_comm
instSMulMemClass 📖	mathematical	—	SMulMemClass NonUnitalSubalgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instSetLike	—	smul_mem'
map_id 📖	mathematical	—	map NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalAlgHom.id	—	SetLike.coe_injective NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Set.image_id
map_injective 📖	mathematical	DFunLike.coe	NonUnitalSubalgebra map	—	ext Set.ext_iff Set.image_injective Set.ext SetLike.ext_iff
map_le 📖	mathematical	—	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	Set.image_subset_iff
map_map 📖	mathematical	—	map NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalAlgHom.comp MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	SetLike.coe_injective NonUnitalAlgHom.instNonUnitalAlgSemiHomClass MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId Set.image_image
map_mono 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	map	—	Set.image_mono
map_toNonUnitalSubsemiring 📖	mathematical	—	toNonUnitalSubsemiring map NonUnitalSubsemiring.map NonUnitalRingHom NonUnitalRingHom.instFunLike NonUnitalRingHom.instNonUnitalRingHomClass NonUnitalRingHomClass.toNonUnitalRingHom NonUnitalAlgHomClass.toNonUnitalRingHomClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid	—	SetLike.coe_injective NonUnitalRingHom.instNonUnitalRingHomClass NonUnitalAlgHomClass.toNonUnitalRingHomClass
map_toSubmodule 📖	mathematical	—	toSubmodule map Submodule.map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMapClass.linearMap NonUnitalAlgHomClass.instLinearMapClass	—	SetLike.coe_injective RingHomSurjective.ids NonUnitalAlgHomClass.instLinearMapClass
mem_carrier 📖	mathematical	—	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.toAddSubsemigroup NonUnitalSubsemiring.toAddSubmonoid toNonUnitalSubsemiring NonUnitalSubalgebra SetLike.instMembership instSetLike	—	—
mem_center_iff 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Subsemigroup.mem_center_iff
mem_centralizer_iff 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike centralizer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
mem_comap 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike comap DFunLike.coe	—	—
mem_map 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership instSetLike map DFunLike.coe	—	NonUnitalSubsemiring.mem_map NonUnitalRingHom.instNonUnitalRingHomClass
mem_prod 📖	mathematical	—	NonUnitalSubalgebra Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership instSetLike prod	—	Set.mem_prod
mem_toNonUnitalSubring 📖	mathematical	—	NonUnitalSubring SetLike.instMembership NonUnitalSubring.instSetLike toNonUnitalSubring NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	—
mem_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubsemiring SetLike.instMembership NonUnitalSubsemiring.instSetLike toNonUnitalSubsemiring NonUnitalSubalgebra instSetLike	—	—
mem_toSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership Submodule.setLike toSubmodule NonUnitalSubalgebra instSetLike	—	—
noZeroDivisors 📖	mathematical	—	NoZeroDivisors NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib toNonUnitalNonAssocSemiring ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass	—	NonUnitalSubsemiringClass.noZeroDivisors instNonUnitalSubsemiringClass
ofClass_carrier 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra instSetLike ofClass	—	—
prod_inf_prod 📖	mathematical	—	NonUnitalSubalgebra Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Prod.isScalarTowerBoth Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Prod.smulCommClassBoth prod	—	SetLike.coe_injective Prod.isScalarTowerBoth Prod.smulCommClassBoth Set.prod_inter_prod
prod_mono 📖	mathematical	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid prod	—	Set.prod_mono
prod_toSubmodule 📖	mathematical	—	toSubmodule Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid prod Submodule.prod	—	—
prod_top 📖	mathematical	—	prod Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.isScalarTowerBoth Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Prod.smulCommClassBoth	—	ext Prod.isScalarTowerBoth Prod.smulCommClassBoth
range_val 📖	mathematical	—	NonUnitalAlgHom.range NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalSubalgebra SetLike.instMembership instSetLike NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass instModule NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalSubalgebraClass.subtype	—	ext instNonUnitalSubsemiringClass NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass Set.ext_iff NonUnitalAlgHom.coe_range Subtype.range_val
smul_mem' 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.toAddSubsemigroup NonUnitalSubsemiring.toAddSubmonoid toNonUnitalSubsemiring	SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	—
subsingleton_of_subsingleton 📖	mathematical	—	NonUnitalSubalgebra	—	ext ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass
toNonUnitalSubring_inj 📖	mathematical	—	toNonUnitalSubring	—	toNonUnitalSubring_injective
toNonUnitalSubring_injective 📖	mathematical	—	NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalSubring toNonUnitalSubring	—	ext mem_toNonUnitalSubring
toNonUnitalSubsemiring_inj 📖	mathematical	—	toNonUnitalSubsemiring	—	toNonUnitalSubsemiring_injective
toNonUnitalSubsemiring_injective 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSubsemiring toNonUnitalSubsemiring	—	smul_mem'
toNonUnitalSubsemiring_subtype 📖	mathematical	—	NonUnitalSubsemiringClass.subtype NonUnitalSubalgebra instSetLike instNonUnitalSubsemiringClass NonUnitalRingHomClass.toNonUnitalRingHom NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHomClass.toNonUnitalRingHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalSubalgebraClass.subtype	—	instNonUnitalSubsemiringClass
toSubmodule_inj 📖	mathematical	—	toSubmodule	—	toSubmodule_injective
toSubmodule_injective 📖	mathematical	—	NonUnitalSubalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toSubmodule	—	SetLike.ext SetLike.ext_iff
toSubmodule_toNonUnitalSubalgebra 📖	mathematical	—	Submodule.toNonUnitalSubalgebra toSubmodule MulMemClass.mul_mem NonUnitalSubalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instSetLike NonUnitalSubsemiringClass.mulMemClass instNonUnitalSubsemiringClass	—	SetLike.coe_injective MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass instNonUnitalSubsemiringClass
toSubring_subtype 📖	mathematical	—	NonUnitalSubringClass.subtype NonUnitalSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring instSetLike instNonUnitalSubringClass NonUnitalRingHomClass.toNonUnitalRingHom NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass NonUnitalSubringClass.toNonUnitalNonAssocRing NonUnitalAlgHom.instFunLike_1 NonUnitalAlgHomClass.toNonUnitalRingHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass NonUnitalSubalgebraClass.subtype	—	instNonUnitalSubringClass

NonUnitalSubalgebra.center

Definitions

Name	Category	Theorems
instNonUnitalCommRing 📖	CompOp	—
instNonUnitalCommSemiring 📖	CompOp	—

NonUnitalSubalgebraClass

Definitions

Name	Category	Theorems
subtype 📖	CompOp	8 math math: coe_subtype, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype, NonUnitalSubalgebra.toSubring_subtype, subtype_injective, NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype, subtype_apply, NonUnitalSubalgebra.range_val, NonUnitalAlgHom.subtype_comp_codRestrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_subtype 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalAlgHom.instFunLike_1 subtype	—	NonUnitalSubsemiringClass.toAddSubmonoidClass
subtype_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalAlgHom.instFunLike_1 subtype	—	NonUnitalSubsemiringClass.toAddSubmonoidClass
subtype_injective 📖	mathematical	—	SetLike.instMembership DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalAlgHom.instFunLike_1 subtype	—	Subtype.coe_injective

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_mem_center 📖	mathematical	Set instMembership center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	commute_iff_eq mul_smul_comm smul_mul_assoc IsMulCentral.comm IsMulCentral.left_assoc IsMulCentral.right_assoc
smul_mem_centralizer 📖	mathematical	Set instMembership centralizer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	mul_smul_comm smul_mul_assoc

Submodule

Definitions

Name	Category	Theorems
toNonUnitalSubalgebra 📖	CompOp	5 math math: NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra, toNonUnitalSubalgebra_toSubmodule, coe_toNonUnitalSubalgebra, toNonUnitalSubalgebra_mk, mem_toNonUnitalSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toNonUnitalSubalgebra 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike toNonUnitalSubalgebra	—	—
mem_toNonUnitalSubalgebra 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike toNonUnitalSubalgebra	—	—
toNonUnitalSubalgebra_mk 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	toNonUnitalSubalgebra AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd AddZeroClass.toAddZero SetLike.coe add_mem zero_mem smul_mem'	—	—
toNonUnitalSubalgebra_toSubmodule 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	NonUnitalSubalgebra.toSubmodule toNonUnitalSubalgebra	—	SetLike.coe_injective

(root)

Definitions

Name	Category	Theorems
nonUnitalSubalgebraOfNonUnitalSubring 📖	CompOp	1 math math: mem_nonUnitalSubalgebraOfNonUnitalSubring
nonUnitalSubalgebraOfNonUnitalSubsemiring 📖	CompOp	1 math math: mem_nonUnitalSubalgebraOfNonUnitalSubsemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_nonUnitalSubalgebraOfNonUnitalSubring 📖	mathematical	—	NonUnitalSubalgebra Int.instCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddCommGroup.toIntModule NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership NonUnitalSubalgebra.instSetLike nonUnitalSubalgebraOfNonUnitalSubring NonUnitalSubring NonUnitalSubring.instSetLike	—	—
mem_nonUnitalSubalgebraOfNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubalgebra Nat.instCommSemiring AddCommMonoid.toNatModule NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership NonUnitalSubalgebra.instSetLike nonUnitalSubalgebraOfNonUnitalSubsemiring NonUnitalSubsemiring NonUnitalSubsemiring.instSetLike	—	—

---

← Back to Index