NonUnitalSubalgebra

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

Statistics

Metric	Count
Definitions codRestrict, equalizer, range, rangeRestrict, adjoin, adjoinNonUnitalCommRingOfComm, adjoinNonUnitalCommSemiringOfComm, gi, instCompleteLatticeNonUnitalStarSubalgebra, instInhabitedNonUnitalStarSubalgebra, toTop, NonUnitalStarSubalgebra, center, centralizer, comap, copy, iSupLift, inclusion, instInhabited, instModule, instNonUnitalCommRing, instNonUnitalCommSemiring, instPartialOrder, instSetLike, map, module', ofClass, prod, toNonUnitalCommRing, toNonUnitalCommSemiring, toNonUnitalRing, toNonUnitalSemiring, toNonUnitalSubalgebra, toNonUnitalSubalgebra', toNonUnitalSubring, subtype, NonUnitalSubalgebra, instInvolutiveStar, starClosure, toNonUnitalStarSubalgebra, ofInjective', ofLeftInverse', instInvolutiveStar, instStarAddMonoid, instStarMul, instStarRing	46
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_eq, adjoin_eq_span, adjoin_eq_starClosure_adjoin, adjoin_induction, adjoin_le, adjoin_le_centralizer_centralizer, adjoin_le_iff, adjoin_mono, adjoin_toNonUnitalSubalgebra, 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_toNonUnitalSubalgebra, inf_toNonUnitalSubalgebra, instIsMulCommutative_adjoin, isMulCommutative_adjoin, isMulCommutative_adjoin_singleton, isMulCommutative_toNonUnitalSubalgebra, 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_toNonUnitalSubalgebra, self_mem_adjoin_singleton, span_eq_toSubmodule, star_self_mem_adjoin_singleton, star_subset_adjoin, subset_adjoin, toNonUnitalSubalgebra_bot, toNonUnitalSubalgebra_eq_top, top_toNonUnitalSubalgebra, center_eq_top, center_toNonUnitalSubalgebra, centralizer_le, centralizer_toNonUnitalSubalgebra, centralizer_univ, coe_add, coe_center, coe_centralizer, coe_centralizer_centralizer, coe_comap, coe_copy, coe_eq_zero, coe_iSup_of_directed, coe_map, coe_mul, coe_neg, coe_prod, coe_smul, coe_sub, coe_toNonUnitalSubalgebra, coe_toNonUnitalSubring, 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, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar, instIsScalarTower, instIsScalarTower', instIsTorsionFree, instNoZeroDivisors, instNonUnitalSubringClass, instNonUnitalSubsemiringClass, instSMulCommClass, instSMulCommClass', instSMulMemClass, instStarMemClass, map_id, map_injective, map_le, map_map, map_mono, map_toNonUnitalSubalgebra, mem_carrier, mem_center_iff, mem_centralizer_iff, mem_comap, mem_map, mem_prod, mem_toNonUnitalSubalgebra, mem_toNonUnitalSubring, ofClass_carrier, prod_inf_prod, prod_mono, prod_toNonUnitalSubalgebra, prod_top, range_val, star_mem', subsingleton_of_subsingleton, toNonUnitalSubalgebra_inj, toNonUnitalSubalgebra_injective, toNonUnitalSubalgebra_le_iff, toNonUnitalSubalgebra_subtype, toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, toNonUnitalSubring_inj, toNonUnitalSubring_injective, toSubring_subtype, val_inclusion, coe_subtype, subtype_apply, subtype_injective, coe_star, coe_starClosure, coe_toNonUnitalStarSubalgebra, mem_starClosure, mem_star_iff, mem_toNonUnitalStarSubalgebra, starClosure_eq_adjoin, starClosure_le, starClosure_le_iff, starClosure_mono, starClosure_toNonUnitalSubalgebra, star_adjoin_comm, star_mem_star_iff, star_mono, toNonUnitalStarSubalgebra_toNonUnitalSubalgebra, ofInjective'_apply, ofLeftInverse'_apply, ofLeftInverse'_symm_apply, instStarModule	162
Total	208

NonUnitalStarAlgHom

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	3 math math: coe_codRestrict, injective_codRestrict, subtype_comp_codRestrict
equalizer 📖	CompOp	1 math math: mem_equalizer
range 📖	CompOp	21 math math: StarAlgEquiv.ofLeftInverse'_apply, range_comp_le_range, range_cfcₙHom, Unitization.starLift_range, NonUnitalStarSubalgebra.range_val, Unitization.inrRangeEquiv_apply_coe_snd, NonUnitalStarAlgebra.range_eq_top, range_cfcₙ_eq_range_cfcₙHom, range_cfcₙHom_le, Unitization.inrRangeEquiv_apply_coe_fst, mem_range_self, cfcₙAux_mem_range_inr, mem_range, NonUnitalStarAlgebra.range_id, NonUnitalStarAlgebra.map_top, StarAlgEquiv.ofInjective'_apply, Unitization.starLift_range_le, StarAlgEquiv.ofLeftInverse'_symm_apply, Unitization.inrRangeEquiv_symm_apply, coe_range, range_comp
rangeRestrict 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_codRestrict 📖	mathematical	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike DFunLike.coe	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instModule StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass instFunLike codRestrict	—	NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instStarMemClass
coe_range 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalStarSubalgebra.instSetLike range Set.range DFunLike.coe	—	—
injective_codRestrict 📖	mathematical	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike DFunLike.coe	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instModule StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass instFunLike codRestrict	—	NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instStarMemClass
map_adjoin 📖	mathematical	—	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarAlgebra.adjoin Set.image DFunLike.coe	—	GaloisConnection.l_comm_of_u_comm Set.image_preimage NonUnitalStarSubalgebra.gc_map_comap GaloisInsertion.gc
map_adjoin_singleton 📖	mathematical	—	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarAlgebra.adjoin Set Set.instSingletonSet DFunLike.coe	—	map_adjoin NonUnitalStarAlgebra.adjoin.congr_simp Set.image_singleton
mem_equalizer 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike equalizer DFunLike.coe	—	—
mem_range 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike range DFunLike.coe	—	NonUnitalRingHom.mem_srange NonUnitalRingHom.instNonUnitalRingHomClass
mem_range_self 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike range DFunLike.coe	—	NonUnitalAlgHom.mem_range
range_comp 📖	mathematical	—	range NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike instNonUnitalAlgHomClass instStarHomClass comp NonUnitalStarSubalgebra.map	—	SetLike.coe_injective instNonUnitalAlgHomClass instStarHomClass Set.range_comp
range_comp_le_range 📖	mathematical	—	NonUnitalStarSubalgebra Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder range NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike instNonUnitalAlgHomClass instStarHomClass comp	—	SetLike.coe_mono instIsConcreteLE instNonUnitalAlgHomClass instStarHomClass Set.range_comp_subset_range
subsingleton 📖	mathematical	—	NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	ext NonUnitalStarAlgebra.mem_top map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgHomClass NonUnitalStarAlgebra.mem_bot
subtype_comp_codRestrict 📖	mathematical	NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike DFunLike.coe	comp NonUnitalStarSubalgebra SetLike.instMembership NonUnitalStarSubalgebra.instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instSMulMemClass StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass NonUnitalStarSubalgebraClass.subtype codRestrict NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom	—	ext NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instSMulMemClass NonUnitalStarSubalgebra.instStarMemClass

NonUnitalStarAlgebra

Definitions

Name	Category	Theorems
adjoin 📖	CompOp	29 math math: NonUnitalStarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, StarAlgebra.adjoin_nonUnitalStarSubalgebra, instIsMulCommutative_adjoin, adjoin_toNonUnitalSubalgebra, isMulCommutative_adjoin_singleton, adjoin_eq_starClosure_adjoin, adjoin_le, adjoin_mono, adjoin_eq_span, gc, subset_adjoin, ContinuousMap.adjoin_id_eq_span_one_union, NonUnitalSubalgebra.starClosure_eq_adjoin, star_subset_adjoin, NonUnitalStarAlgHom.map_adjoin_singleton, isMulCommutative_adjoin, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, mem_adjoin_of_mem, ContinuousMap.adjoin_id_eq_span_one_add, adjoin_le_iff, adjoin_eq, NonUnitalStarAlgHom.map_adjoin, star_self_mem_adjoin_singleton, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, self_mem_adjoin_singleton, ContinuousMapZero.adjoin_id_dense, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, adjoin_le_starAlgebra_adjoin, adjoin_le_centralizer_centralizer
adjoinNonUnitalCommRingOfComm 📖	CompOp	—
adjoinNonUnitalCommSemiringOfComm 📖	CompOp	—
gi 📖	CompOp	—
instCompleteLatticeNonUnitalStarSubalgebra 📖	CompOp	33 math math: mem_bot, mem_sup_right, coe_bot, mem_top, mem_sInf, iInf_toNonUnitalSubalgebra, coe_top, coe_sInf, mem_iInf, top_toNonUnitalSubalgebra, range_eq_top, toNonUnitalSubalgebra_eq_top, mul_mem_sup, mem_sup_left, NonUnitalStarSubalgebra.prod_inf_prod, comap_top, coe_iInf, map_bot, NonUnitalStarSubalgebra.coe_iSup_of_directed, coe_inf, map_sup, range_id, map_top, NonUnitalStarSubalgebra.center_eq_top, eq_top_iff, map_inf, NonUnitalStarSubalgebra.prod_top, ContinuousMapZero.elemental_eq_top, sInf_toNonUnitalSubalgebra, toNonUnitalSubalgebra_bot, mem_inf, map_iInf, inf_toNonUnitalSubalgebra
instInhabitedNonUnitalStarSubalgebra 📖	CompOp	—
toTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq 📖	mathematical	—	adjoin SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike	—	le_antisymm adjoin_le le_rfl subset_adjoin
adjoin_eq_span 📖	mathematical	—	NonUnitalSubalgebra.toSubmodule NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra.toNonUnitalSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid adjoin Submodule.span CommSemiring.toSemiring SetLike.coe Subsemigroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Subsemigroup.instSetLike Subsemigroup.closure Set Set.instUnion Star.star Set.star	—	adjoin_toNonUnitalSubalgebra NonUnitalAlgebra.adjoin_eq_span
adjoin_eq_starClosure_adjoin 📖	mathematical	—	adjoin NonUnitalSubalgebra.starClosure NonUnitalAlgebra.adjoin NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective NonUnitalAlgebra.adjoin_union NonUnitalSubalgebra.star_adjoin_comm
adjoin_induction 📖	—	subset_adjoin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring AddMemClass.add_mem NonUnitalStarSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.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 NonUnitalStarSubalgebra.instSMulMemClass Star.star StarMemClass.star_mem NonUnitalStarSubalgebra.instStarMemClass SetLike.instMembership	—	—	subset_adjoin AddMemClass.add_mem AddSubmonoidClass.toAddMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass SMulMemClass.smul_mem NonUnitalStarSubalgebra.instSMulMemClass StarMemClass.star_mem NonUnitalStarSubalgebra.instStarMemClass NonUnitalAlgebra.adjoin_induction NonUnitalAlgebra.subset_adjoin star_star
adjoin_le 📖	mathematical	Set Set.instHasSubset SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder adjoin	—	GaloisConnection.l_le gc
adjoin_le_centralizer_centralizer 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder adjoin NonUnitalStarSubalgebra.centralizer SetLike.coe NonUnitalStarSubalgebra.instSetLike	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra adjoin_toNonUnitalSubalgebra StarMemClass.star_coe_eq NonUnitalStarSubalgebra.instStarMemClass Set.union_self NonUnitalAlgebra.adjoin_le_centralizer_centralizer
adjoin_le_iff 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder adjoin Set Set.instHasSubset SetLike.coe NonUnitalStarSubalgebra.instSetLike	—	gc
adjoin_mono 📖	mathematical	Set Set.instHasSubset	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder adjoin	—	GaloisConnection.monotone_l gc
adjoin_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid adjoin NonUnitalAlgebra.adjoin Set Set.instUnion Star.star Set.star	—	—
coe_bot 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Zero.instNonempty
coe_iInf 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra Set.iInter	—	coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.iInter_iInter_eq'
coe_inf 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra Set Set.instInter	—	—
coe_sInf 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra Set.iInter Set Set.instMembership	—	sInf_image
coe_top 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
comap_top 📖	mathematical	—	NonUnitalStarSubalgebra.comap NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff mem_top
commute_of_mem_adjoin_of_forall_mem_commute 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute star_star
commute_of_mem_adjoin_self 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Set Set.instSingletonSet	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	commute_of_mem_adjoin_singleton_of_commute Commute.symm isStarNormal_iff
commute_of_mem_adjoin_singleton_of_commute 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Set Set.instSingletonSet Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	commute_of_mem_adjoin_of_forall_mem_commute
eq_top_iff 📖	mathematical	—	Top.top NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder SetLike.instMembership NonUnitalStarSubalgebra.instSetLike	—	mem_top NonUnitalStarSubalgebra.ext
gc 📖	mathematical	—	GaloisConnection Set NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra NonUnitalStarSubalgebra.instPartialOrder adjoin SetLike.coe NonUnitalStarSubalgebra.instSetLike	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff adjoin_toNonUnitalSubalgebra NonUnitalAlgebra.adjoin_le_iff NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left Set.union_subset StarMemClass.star_mem NonUnitalStarSubalgebra.instStarMemClass star_star
iInf_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid iInf NonUnitalStarSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra NonUnitalSubalgebra NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	—	SetLike.coe_injective coe_iInf NonUnitalAlgebra.coe_iInf
inf_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra NonUnitalSubalgebra NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	—	SetLike.coe_injective coe_inf
instIsMulCommutative_adjoin 📖	mathematical	—	IsMulCommutative NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin SetLike.coe Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring	—	isMulCommutative_adjoin setLike_mul_comm StarMemClass.star_mem
isMulCommutative_adjoin 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	IsMulCommutative NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring	—	adjoin_le_centralizer_centralizer IsMulCommutative.of_setLike_mul_comm NonUnitalSubsemiringClass.mulMemClass Set.union_star_self_comm Set.centralizer_centralizer_comm_of_comm NonUnitalStarSubalgebra.coe_centralizer_centralizer SetLike.mem_coe
isMulCommutative_adjoin_singleton 📖	mathematical	—	IsMulCommutative NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring	—	isMulCommutative_adjoin
isMulCommutative_toNonUnitalSubalgebra 📖	mathematical	—	IsMulCommutative NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubalgebra.instSetLike NonUnitalStarSubalgebra.toNonUnitalSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSubalgebra.toNonUnitalNonAssocSemiring	—	—
map_bot 📖	mathematical	—	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Bot.bot NonUnitalStarSubalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	SetLike.coe_injective coe_bot Set.image_singleton map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass
map_iInf 📖	mathematical	DFunLike.coe	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid iInf NonUnitalStarSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	SetLike.coe_injective coe_iInf Set.InjOn.image_iInter_eq Set.injOn_of_injective
map_inf 📖	mathematical	DFunLike.coe	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	SetLike.coe_injective Set.image_inter
map_sup 📖	mathematical	—	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	GaloisConnection.l_sup NonUnitalStarSubalgebra.gc_map_comap
map_top 📖	mathematical	—	NonUnitalStarSubalgebra.map NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalStarAlgHom.range	—	SetLike.coe_injective Set.image_univ
mem_adjoin_of_mem 📖	mathematical	Set Set.instMembership	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin	—	subset_adjoin
mem_bot 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Set.star_empty Set.union_empty NonUnitalAlgebra.adjoin_empty NonUnitalAlgebra.mem_bot
mem_iInf 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	—
mem_inf 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	—
mem_sInf 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	coe_sInf
mem_sup_left 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	SetLike.le_def instIsConcreteLE le_sup_left
mem_sup_right 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra	—	SetLike.le_def instIsConcreteLE le_sup_right
mem_top 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_univ
mul_mem_sup 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulMemClass.mul_mem NonUnitalSubsemiringClass.mulMemClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass mem_sup_left mem_sup_right
range_eq_top 📖	mathematical	—	NonUnitalStarAlgHom.range NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe	—	eq_top_iff
range_id 📖	mathematical	—	NonUnitalStarAlgHom.range NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarAlgHom.id Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass Set.range_id
sInf_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid InfSet.sInf NonUnitalStarSubalgebra ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeNonUnitalStarSubalgebra NonUnitalSubalgebra NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Set.image	—	SetLike.coe_injective coe_sInf NonUnitalAlgebra.coe_sInf Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
self_mem_adjoin_singleton 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Set Set.instSingletonSet	—	NonUnitalAlgebra.subset_adjoin Set.mem_union_left Set.mem_singleton
span_eq_toSubmodule 📖	mathematical	—	Submodule.span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.coe NonUnitalStarSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike NonUnitalSubalgebra.toSubmodule NonUnitalStarSubalgebra.toNonUnitalSubalgebra	—	Submodule.coe_span_eq_self NonUnitalSubsemiringClass.toAddSubmonoidClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instSMulMemClass
star_self_mem_adjoin_singleton 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike adjoin Set Set.instSingletonSet Star.star	—	StarMemClass.star_mem NonUnitalStarSubalgebra.instStarMemClass self_mem_adjoin_singleton
star_subset_adjoin 📖	mathematical	—	Set Set.instHasSubset Star.star Set.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid SetLike.coe NonUnitalStarSubalgebra NonUnitalStarSubalgebra.instSetLike adjoin	—	HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_right NonUnitalAlgebra.subset_adjoin
subset_adjoin 📖	mathematical	—	Set Set.instHasSubset SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike adjoin	—	HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left NonUnitalAlgebra.subset_adjoin
toNonUnitalSubalgebra_bot 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Bot.bot NonUnitalStarSubalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder NonUnitalSubalgebra NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	—	NonUnitalSubalgebra.ext
toNonUnitalSubalgebra_eq_top 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Top.top NonUnitalSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalStarSubalgebra instCompleteLatticeNonUnitalStarSubalgebra	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective top_toNonUnitalSubalgebra
top_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Top.top NonUnitalStarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder NonUnitalSubalgebra NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra	—	NonUnitalSubalgebra.ext

NonUnitalStarSubalgebra

Definitions

Name	Category	Theorems
center 📖	CompOp	5 math math: center_toNonUnitalSubalgebra, mem_center_iff, coe_center, center_eq_top, centralizer_univ
centralizer 📖	CompOp	9 math math: centralizer_le, topologicalClosure_adjoin_le_centralizer_centralizer, coe_centralizer, mem_centralizer_iff, NonUnitalStarAlgebra.elemental.le_centralizer_centralizer, coe_centralizer_centralizer, centralizer_toNonUnitalSubalgebra, centralizer_univ, NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer
comap 📖	CompOp	5 math math: mem_comap, NonUnitalStarAlgebra.comap_top, gc_map_comap, map_le, coe_comap
copy 📖	CompOp	2 math math: copy_eq, coe_copy
iSupLift 📖	CompOp	4 math math: iSupLift_inclusion, iSupLift_of_mem, iSupLift_comp_inclusion, iSupLift_mk
inclusion 📖	CompOp	8 math math: val_inclusion, inclusion_mk, iSupLift_inclusion, inclusion_right, iSupLift_comp_inclusion, inclusion_injective, inclusion_self, inclusion_inclusion
instInhabited 📖	CompOp	—
instModule 📖	CompOp	24 math math: StarAlgEquiv.ofLeftInverse'_apply, NonUnitalStarAlgHom.coe_codRestrict, NonUnitalStarAlgHom.injective_codRestrict, val_inclusion, instIsTorsionFree, range_val, inclusion_mk, Unitization.inrRangeEquiv_apply_coe_snd, iSupLift_inclusion, Unitization.inrRangeEquiv_apply_coe_fst, iSupLift_of_mem, inclusion_right, instSMulCommClass', iSupLift_comp_inclusion, StarAlgEquiv.ofInjective'_apply, instIsScalarTower, inclusion_injective, StarAlgEquiv.ofLeftInverse'_symm_apply, instSMulCommClass, Unitization.inrRangeEquiv_symm_apply, iSupLift_mk, inclusion_self, instIsScalarTower', inclusion_inclusion
instNonUnitalCommRing 📖	CompOp	—
instNonUnitalCommSemiring 📖	CompOp	—
instPartialOrder 📖	CompOp	29 math math: topologicalClosure_map_le, centralizer_le, topologicalClosure_adjoin_le_centralizer_centralizer, topologicalClosure_minimal, NonUnitalSubalgebra.starClosure_le_iff, NonUnitalStarAlgHom.range_comp_le_range, map_mono, NonUnitalStarAlgebra.adjoin_le, NonUnitalStarAlgebra.adjoin_mono, NonUnitalStarAlgebra.gc, NonUnitalSubalgebra.starClosure_mono, topologicalClosure_mono, range_cfcₙHom_le, NonUnitalSubalgebra.starClosure_le, prod_mono, NonUnitalStarAlgebra.elemental.le_centralizer_centralizer, toNonUnitalSubalgebra_le_iff, le_topologicalClosure, gc_map_comap, NonUnitalStarAlgebra.adjoin_le_iff, NonUnitalStarAlgebra.elemental.le_of_mem, NonUnitalStarAlgebra.elemental.le_iff_mem, Unitization.starLift_range_le, map_le, map_topologicalClosure_le, NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin, inclusion_self, inclusion_inclusion, NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer
instSetLike 📖	CompOp	130 math math: range_cfcₙ_nnreal, NonUnitalSubalgebra.coe_starClosure, mem_carrier, coe_zero, ofClass_carrier, mem_map, instSMulMemClass, StarAlgEquiv.ofLeftInverse'_apply, cfcₙHom_apply_mem_elemental, NonUnitalStarAlgHom.coe_codRestrict, NonUnitalStarAlgebra.mem_bot, topologicalClosure_adjoin_le_centralizer_centralizer, NonUnitalStarAlgebra.mem_sup_right, NonUnitalStarAlgebra.coe_bot, NonUnitalStarAlgebra.mem_top, NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra, NonUnitalStarAlgebra.elemental.isClosedEmbedding_coe, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar, StarSubalgebra.mem_toNonUnitalStarSubalgebra, coe_copy, mem_comap, cfcₙHom_mem_elemental, coe_neg, NonUnitalStarAlgebra.mem_sInf, StarAlgebra.adjoin_nonUnitalStarSubalgebra, instNonUnitalSubringClass, NonUnitalStarAlgebra.instIsMulCommutative_adjoin, NonUnitalStarAlgHom.injective_codRestrict, NonUnitalStarAlgebra.coe_top, coe_toNonUnitalSubring, NonUnitalStarAlgebra.coe_sInf, val_inclusion, instIsTopologicalSemiring, NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, range_cfcₙ, cfcₙ_mem_elemental, instIsTorsionFree, Unitization.starLift_range, mem_toNonUnitalSubring, NonUnitalStarAlgebra.mem_iInf, ext_iff, NonUnitalStarAlgebra.gc, NonUnitalStarAlgebra.subset_adjoin, toNonUnitalSubalgebra_subtype, range_val, NonUnitalStarAlgebra.elemental.isClosed, inclusion_mk, NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra, Unitization.inrRangeEquiv_apply_coe_snd, coe_centralizer, range_cfcₙ_eq_range_cfcₙHom, ContinuousMap.adjoin_id_eq_span_one_union, iSupLift_inclusion, mem_centralizer_iff, Unitization.inrRangeEquiv_apply_coe_fst, NonUnitalStarAlgebra.elemental.self_mem, NonUnitalStarAlgebra.star_subset_adjoin, NonUnitalStarAlgebra.mul_mem_sup, instNonUnitalSubsemiringClass, NonUnitalStarAlgebra.mem_sup_left, coe_map, NonUnitalStarAlgebra.elemental.le_centralizer_centralizer, iSupLift_of_mem, instIsSemitopologicalRing, NonUnitalStarAlgebra.elemental.star_self_mem, coe_eq_zero, NonUnitalStarAlgebra.isMulCommutative_adjoin, NonUnitalStarAlgHom.mem_range_self, NonUnitalStarAlgebra.coe_iInf, range_cfcₙ_subset, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, mem_center_iff, coe_center, instIsTopologicalRing, inclusion_right, coe_smul, range_cfcₙ_nnreal_subset, instSMulCommClass', iSupLift_comp_inclusion, coe_centralizer_centralizer, coe_iSup_of_directed, NonUnitalStarAlgebra.mem_adjoin_of_mem, toSubring_subtype, NonUnitalStarAlgHom.mem_equalizer, cfcₙAux_mem_range_inr, ContinuousMap.adjoin_id_eq_span_one_add, NonUnitalStarAlgebra.adjoin_le_iff, NonUnitalStarAlgebra.span_eq_toSubmodule, instNoZeroDivisors, NonUnitalStarAlgHom.mem_range, NonUnitalStarAlgebra.coe_inf, NonUnitalStarAlgHom.subtype_comp_codRestrict, NonUnitalStarAlgebra.adjoin_eq, coe_mul, StarSubalgebra.one_mem_toNonUnitalStarSubalgebra, toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, coe_toNonUnitalSubalgebra, NonUnitalStarAlgebra.star_self_mem_adjoin_singleton, NonUnitalStarAlgebra.elemental.le_iff_mem, coe_add, instIsSemitopologicalSemiring, StarAlgEquiv.ofInjective'_apply, coe_prod, NonUnitalStarAlgebra.eq_top_iff, instIsScalarTower, inclusion_injective, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, NonUnitalStarAlgebra.self_mem_adjoin_singleton, cfcₙ_apply_mem_elemental, ContinuousMapZero.adjoin_id_dense, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, StarAlgEquiv.ofLeftInverse'_symm_apply, coe_sub, NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra, instSMulCommClass, Unitization.inrRangeEquiv_symm_apply, mem_prod, mem_toNonUnitalSubalgebra, iSupLift_mk, inclusion_self, NonUnitalSubalgebra.mem_starClosure, instIsScalarTower', coe_comap, NonUnitalStarAlgebra.mem_inf, inclusion_inclusion, instStarMemClass, NonUnitalStarAlgHom.coe_range, NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer, isClosed_topologicalClosure
map 📖	CompOp	20 math math: topologicalClosure_map_le, mem_map, map_map, map_mono, coe_map, NonUnitalStarAlgHom.map_adjoin_singleton, gc_map_comap, NonUnitalStarAlgebra.map_bot, map_injective, NonUnitalStarAlgebra.map_sup, NonUnitalStarAlgebra.map_top, NonUnitalStarAlgHom.map_adjoin, NonUnitalStarAlgebra.map_inf, topologicalClosure_map, map_le, map_topologicalClosure_le, map_toNonUnitalSubalgebra, map_id, NonUnitalStarAlgebra.map_iInf, NonUnitalStarAlgHom.range_comp
module' 📖	CompOp	2 math math: instSMulCommClass', instIsScalarTower'
ofClass 📖	CompOp	1 math math: ofClass_carrier
prod 📖	CompOp	6 math math: prod_toNonUnitalSubalgebra, prod_mono, prod_inf_prod, coe_prod, prod_top, mem_prod
toNonUnitalCommRing 📖	CompOp	—
toNonUnitalCommSemiring 📖	CompOp	—
toNonUnitalRing 📖	CompOp	2 math math: instIsSemitopologicalRing, instIsTopologicalRing
toNonUnitalSemiring 📖	CompOp	22 math math: StarAlgEquiv.ofLeftInverse'_apply, NonUnitalStarAlgebra.instIsMulCommutative_adjoin, val_inclusion, instIsTopologicalSemiring, NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton, inclusion_mk, Unitization.inrRangeEquiv_apply_coe_snd, iSupLift_inclusion, Unitization.inrRangeEquiv_apply_coe_fst, iSupLift_of_mem, NonUnitalStarAlgebra.isMulCommutative_adjoin, inclusion_right, iSupLift_comp_inclusion, instNoZeroDivisors, instIsSemitopologicalSemiring, StarAlgEquiv.ofInjective'_apply, inclusion_injective, StarAlgEquiv.ofLeftInverse'_symm_apply, Unitization.inrRangeEquiv_symm_apply, iSupLift_mk, inclusion_self, inclusion_inclusion
toNonUnitalSubalgebra 📖	CompOp	26 math math: mem_carrier, prod_toNonUnitalSubalgebra, NonUnitalSubalgebra.starClosure_le_iff, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, center_toNonUnitalSubalgebra, NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra, toNonUnitalSubalgebra_injective, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, NonUnitalStarAlgebra.adjoin_eq_span, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, toNonUnitalSubalgebra_le_iff, toNonUnitalSubalgebra_inj, centralizer_toNonUnitalSubalgebra, NonUnitalStarAlgebra.span_eq_toSubmodule, star_mem', toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, coe_toNonUnitalSubalgebra, NonUnitalSubalgebra.toNonUnitalStarSubalgebra_toNonUnitalSubalgebra, NonUnitalStarAlgebra.isMulCommutative_toNonUnitalSubalgebra, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, map_toNonUnitalSubalgebra, mem_toNonUnitalSubalgebra, NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra
toNonUnitalSubalgebra' 📖	CompOp	—
toNonUnitalSubring 📖	CompOp	4 math math: coe_toNonUnitalSubring, toNonUnitalSubring_inj, mem_toNonUnitalSubring, toNonUnitalSubring_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_top 📖	mathematical	—	center NonUnitalCommSemiring.toNonUnitalSemiring Top.top NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective Set.center_eq_univ
center_toNonUnitalSubalgebra 📖	mathematical	—	toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid center NonUnitalSubalgebra.center	—	—
centralizer_le 📖	mathematical	Set Set.instHasSubset	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	Set.centralizer_subset Set.union_subset_union Set.preimage_mono
centralizer_toNonUnitalSubalgebra 📖	mathematical	—	toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid centralizer NonUnitalSubalgebra.centralizer Set Set.instUnion Star.star Set.instInvolutiveStar	—	—
centralizer_univ 📖	mathematical	—	centralizer Set.univ center	—	SetLike.ext' coe_centralizer Set.univ_union coe_center Set.centralizer_univ
coe_add 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass	—	instNonUnitalSubsemiringClass
coe_center 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instSetLike center Set.center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_centralizer 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instSetLike centralizer Set.centralizer Set Set.instUnion Star.star Set.instInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_centralizer_centralizer 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instSetLike centralizer Set.centralizer Set Set.instUnion Star.star Set.instInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	coe_centralizer StarMemClass.star_coe_eq instStarMemClass Set.union_self
coe_comap 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra instSetLike comap Set.preimage DFunLike.coe	—	—
coe_copy 📖	mathematical	SetLike.coe NonUnitalStarSubalgebra instSetLike	SetLike.coe NonUnitalStarSubalgebra instSetLike copy	—	—
coe_eq_zero 📖	mathematical	—	NonUnitalStarSubalgebra 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 NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra Set.iUnion	—	NonUnitalSubalgebra.coe_iSup_of_directed Set.mem_iUnion StarMemClass.star_mem instStarMemClass le_antisymm iSup_le le_iSup Set.iUnion_subset
coe_map 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra instSetLike map Set.image DFunLike.coe	—	—
coe_mul 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass	—	instNonUnitalSubsemiringClass
coe_neg 📖	mathematical	—	NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClass	—	NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClass
coe_prod 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra Prod.instNonUnitalNonAssocSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid instSetLike prod SProd.sprod Set Set.instSProd	—	—
coe_smul 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike SetLike.smul' MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction instSMulMemClass	—	instSMulMemClass
coe_sub 📖	mathematical	—	NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike AddSubgroupClass.sub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalSubringClass.addSubgroupClass instNonUnitalSubringClass SubNegMonoid.toSub	—	NonUnitalSubringClass.addSubgroupClass instNonUnitalSubringClass
coe_toNonUnitalSubalgebra 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSubalgebra.instSetLike toNonUnitalSubalgebra NonUnitalStarSubalgebra instSetLike	—	—
coe_toNonUnitalSubring 📖	mathematical	—	SetLike.coe NonUnitalSubring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSubring.instSetLike toNonUnitalSubring NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	—
coe_zero 📖	mathematical	—	NonUnitalStarSubalgebra 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 NonUnitalStarSubalgebra instSetLike	copy	—	SetLike.coe_injective
ext 📖	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike	—	ext
gc_map_comap 📖	mathematical	—	GaloisConnection NonUnitalStarSubalgebra PartialOrder.toPreorder instPartialOrder map comap	—	map_le
iSupLift_comp_inclusion 📖	mathematical	Directed NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalStarAlgHom.comp SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass inclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra	NonUnitalStarAlgHom.comp NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass iSupLift inclusion	—	instStarMemClass NonUnitalStarAlgHom.ext iSupLift_inclusion
iSupLift_inclusion 📖	mathematical	Directed NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalStarAlgHom.comp SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass inclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike iSupLift inclusion	—	instStarMemClass Set.iUnionLift_inclusion
iSupLift_mk 📖	mathematical	Directed NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalStarAlgHom.comp SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass inclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike iSupLift	—	instStarMemClass
iSupLift_of_mem 📖	mathematical	Directed NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalStarAlgHom.comp SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass inclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike iSupLift	—	instStarMemClass Set.iUnionLift_of_mem
inclusion_inclusion 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike inclusion le_trans PartialOrder.toPreorder instPartialOrder	—	instStarMemClass le_trans
inclusion_injective 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike inclusion	—	instStarMemClass
inclusion_mk 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike inclusion	—	instStarMemClass
inclusion_right 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	DFunLike.coe NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike inclusion	—	instStarMemClass
inclusion_self 📖	mathematical	—	NonUnitalAlgHomClass.toNonUnitalAlgHom NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass inclusion le_refl PartialOrder.toPreorder instPartialOrder NonUnitalAlgHom.id	—	NonUnitalAlgHom.ext instStarMemClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass le_refl
instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar 📖	mathematical	—	CanLift Set NonUnitalStarSubalgebra SetLike.coe instSetLike Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
instIsScalarTower 📖	mathematical	—	IsScalarTower NonUnitalStarSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule instDistribSMul	—	instNonUnitalSubsemiringClass smul_assoc
instIsScalarTower' 📖	mathematical	—	IsScalarTower NonUnitalStarSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule module'	—	NonUnitalSubalgebra.instIsScalarTower'
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree NonUnitalStarSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass instModule	—	Function.Injective.moduleIsTorsionFree instNonUnitalSubsemiringClass Subtype.coe_injective
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib toNonUnitalSemiring ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass	—	NonUnitalSubsemiringClass.noZeroDivisors instNonUnitalSubsemiringClass
instNonUnitalSubringClass 📖	mathematical	—	NonUnitalSubringClass NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	instNonUnitalSubsemiringClass SMulMemClass.smul_mem instSMulMemClass neg_one_smul
instNonUnitalSubsemiringClass 📖	mathematical	—	NonUnitalSubsemiringClass NonUnitalStarSubalgebra instSetLike	—	AddSubsemigroup.add_mem' AddSubmonoid.zero_mem' NonUnitalSubsemiring.mul_mem'
instSMulCommClass 📖	mathematical	—	SMulCommClass NonUnitalStarSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction instModule instDistribSMul	—	instNonUnitalSubsemiringClass SMulCommClass.smul_comm
instSMulCommClass' 📖	mathematical	—	SMulCommClass NonUnitalStarSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction module' CommSemiring.toSemiring instModule	—	instNonUnitalSubsemiringClass SMulCommClass.smul_comm
instSMulMemClass 📖	mathematical	—	SMulMemClass NonUnitalStarSubalgebra 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	—	NonUnitalSubalgebra.smul_mem'
instStarMemClass 📖	mathematical	—	StarMemClass NonUnitalStarSubalgebra instSetLike	—	star_mem'
map_id 📖	mathematical	—	map NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarAlgHom.id	—	SetLike.coe_injective NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass Set.image_id
map_injective 📖	mathematical	DFunLike.coe	NonUnitalStarSubalgebra map	—	ext Set.ext_iff Set.image_injective Set.ext SetLike.ext_iff
map_le 📖	mathematical	—	NonUnitalStarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	Set.image_subset_iff
map_map 📖	mathematical	—	map NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarAlgHom.comp	—	SetLike.coe_injective NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass Set.image_image
map_mono 📖	mathematical	NonUnitalStarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	NonUnitalStarSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder map	—	Set.image_mono
map_toNonUnitalSubalgebra 📖	mathematical	—	toNonUnitalSubalgebra map NonUnitalSubalgebra.map	—	SetLike.coe_injective
mem_carrier 📖	mathematical	—	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.toAddSubsemigroup NonUnitalSubsemiring.toAddSubmonoid NonUnitalSubalgebra.toNonUnitalSubsemiring toNonUnitalSubalgebra NonUnitalStarSubalgebra SetLike.instMembership instSetLike	—	—
mem_center_iff 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Subsemigroup.mem_center_iff
mem_centralizer_iff 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike centralizer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star	—	Set.star_mem_star star_star
mem_comap 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike comap DFunLike.coe	—	—
mem_map 📖	mathematical	—	NonUnitalStarSubalgebra SetLike.instMembership instSetLike map DFunLike.coe	—	NonUnitalSubalgebra.mem_map NonUnitalAlgHom.instNonUnitalAlgSemiHomClass
mem_prod 📖	mathematical	—	NonUnitalStarSubalgebra Prod.instNonUnitalNonAssocSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike prod	—	Set.mem_prod
mem_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalSubalgebra SetLike.instMembership NonUnitalSubalgebra.instSetLike toNonUnitalSubalgebra NonUnitalStarSubalgebra instSetLike	—	—
mem_toNonUnitalSubring 📖	mathematical	—	NonUnitalSubring NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership NonUnitalSubring.instSetLike toNonUnitalSubring NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike	—	—
ofClass_carrier 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra instSetLike ofClass	—	—
prod_inf_prod 📖	mathematical	—	NonUnitalStarSubalgebra Prod.instNonUnitalNonAssocSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra Prod.instNonUnitalSemiring Prod.instStarRing Prod.isScalarTowerBoth Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction Prod.smulCommClassBoth Prod.instStarModule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring prod	—	SetLike.coe_injective Prod.isScalarTowerBoth Prod.smulCommClassBoth Prod.instStarModule Set.prod_inter_prod
prod_mono 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	NonUnitalStarSubalgebra Prod.instNonUnitalNonAssocSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder prod	—	Set.prod_mono
prod_toNonUnitalSubalgebra 📖	mathematical	—	toNonUnitalSubalgebra Prod.instNonUnitalNonAssocSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid prod NonUnitalSubalgebra.prod	—	—
prod_top 📖	mathematical	—	prod Top.top NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Prod.instNonUnitalNonAssocSemiring Prod.instModule CommSemiring.toSemiring Prod.instStar Prod.instNonUnitalSemiring Prod.instStarRing Prod.isScalarTowerBoth Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction Prod.smulCommClassBoth Prod.instStarModule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ext Prod.isScalarTowerBoth Prod.smulCommClassBoth Prod.instStarModule
range_val 📖	mathematical	—	NonUnitalStarAlgHom.range NonUnitalStarAlgHom NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass Module.toDistribMulAction SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass StarMemClass.instStar instStarMemClass instModule NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarSubalgebraClass.subtype	—	ext instNonUnitalSubsemiringClass NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass instStarMemClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass Set.ext_iff NonUnitalStarAlgHom.coe_range Subtype.range_val
star_mem' 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.toAddSubsemigroup NonUnitalSubsemiring.toAddSubmonoid NonUnitalSubalgebra.toNonUnitalSubsemiring toNonUnitalSubalgebra	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.toAddSubsemigroup NonUnitalSubsemiring.toAddSubmonoid NonUnitalSubalgebra.toNonUnitalSubsemiring toNonUnitalSubalgebra Star.star	—	—
subsingleton_of_subsingleton 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	ext ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass NonUnitalSubsemiringClass.toAddSubmonoidClass instNonUnitalSubsemiringClass
toNonUnitalSubalgebra_inj 📖	mathematical	—	toNonUnitalSubalgebra	—	toNonUnitalSubalgebra_injective
toNonUnitalSubalgebra_injective 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSubalgebra toNonUnitalSubalgebra	—	ext mem_toNonUnitalSubalgebra
toNonUnitalSubalgebra_le_iff 📖	mathematical	—	NonUnitalSubalgebra Preorder.toLE PartialOrder.toPreorder NonUnitalSubalgebra.instPartialOrder toNonUnitalSubalgebra NonUnitalStarSubalgebra instPartialOrder	—	—
toNonUnitalSubalgebra_subtype 📖	mathematical	—	NonUnitalSubalgebraClass.subtype NonUnitalStarSubalgebra instSetLike instNonUnitalSubsemiringClass instSMulMemClass NonUnitalAlgHomClass.toNonUnitalAlgHom NonUnitalStarAlgHom SetLike.instMembership MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarSubalgebraClass.subtype	—	instNonUnitalSubsemiringClass NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass
toNonUnitalSubalgebra_toNonUnitalStarSubalgebra 📖	mathematical	—	NonUnitalSubalgebra.toNonUnitalStarSubalgebra toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring StarMemClass.star_mem NonUnitalStarSubalgebra instSetLike instStarMemClass	—	SetLike.coe_injective StarMemClass.star_mem instStarMemClass
toNonUnitalSubring_inj 📖	mathematical	—	toNonUnitalSubring	—	toNonUnitalSubring_injective
toNonUnitalSubring_injective 📖	mathematical	—	NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSubring toNonUnitalSubring	—	ext mem_toNonUnitalSubring
toSubring_subtype 📖	mathematical	—	NonUnitalSubringClass.subtype NonUnitalStarSubalgebra CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instSetLike instNonUnitalSubringClass NonUnitalRingHomClass.toNonUnitalRingHom NonUnitalStarAlgHom SetLike.instMembership MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring instNonUnitalSubsemiringClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass instSMulMemClass StarMemClass.instStar instStarMemClass NonUnitalSubringClass.toNonUnitalNonAssocRing NonUnitalStarAlgHom.instFunLike NonUnitalAlgHomClass.toNonUnitalRingHomClass MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarSubalgebraClass.subtype	—	instNonUnitalSubringClass
val_inclusion 📖	mathematical	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership instSetLike DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toNonUnitalSemiring Module.toDistribMulAction instModule StarMemClass.instStar instStarMemClass NonUnitalStarAlgHom.instFunLike inclusion	—	instStarMemClass

NonUnitalStarSubalgebraClass

Definitions

Name	Category	Theorems
subtype 📖	CompOp	7 math math: NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype, NonUnitalStarSubalgebra.range_val, coe_subtype, subtype_injective, NonUnitalStarSubalgebra.toSubring_subtype, NonUnitalStarAlgHom.subtype_comp_codRestrict, subtype_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_subtype 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom SetLike.instMembership MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass StarMemClass.instStar NonUnitalStarAlgHom.instFunLike subtype	—	NonUnitalSubsemiringClass.toAddSubmonoidClass
subtype_apply 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom SetLike.instMembership MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass StarMemClass.instStar NonUnitalStarAlgHom.instFunLike subtype	—	NonUnitalSubsemiringClass.toAddSubmonoidClass
subtype_injective 📖	mathematical	—	SetLike.instMembership DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid SubmoduleClass.module NonUnitalSubsemiringClass.toAddSubmonoidClass StarMemClass.instStar NonUnitalStarAlgHom.instFunLike subtype	—	Subtype.coe_injective

NonUnitalSubalgebra

Definitions

Name	Category	Theorems
instInvolutiveStar 📖	CompOp	8 math math: coe_starClosure, mem_star_iff, coe_star, star_mono, starClosure_toNonUnitalSubalgebra, mem_starClosure, star_mem_star_iff, star_adjoin_comm
starClosure 📖	CompOp	8 math math: coe_starClosure, starClosure_le_iff, NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin, starClosure_mono, starClosure_eq_adjoin, starClosure_le, starClosure_toNonUnitalSubalgebra, mem_starClosure
toNonUnitalStarSubalgebra 📖	CompOp	4 math math: coe_toNonUnitalStarSubalgebra, mem_toNonUnitalStarSubalgebra, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, toNonUnitalStarSubalgebra_toNonUnitalSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_star 📖	mathematical	—	SetLike.coe NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring instSetLike Star.star InvolutiveStar.toStar instInvolutiveStar Set Set.star StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	—
coe_starClosure 📖	mathematical	—	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalStarSubalgebra.instSetLike starClosure NonUnitalSubalgebra instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Star.star instInvolutiveStar	—	—
coe_toNonUnitalStarSubalgebra 📖	mathematical	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Star.star	SetLike.coe NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra.instSetLike toNonUnitalStarSubalgebra NonUnitalSubalgebra instSetLike	—	—
mem_starClosure 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SetLike.instMembership NonUnitalStarSubalgebra.instSetLike starClosure NonUnitalSubalgebra instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Star.star instInvolutiveStar	—	—
mem_star_iff 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Star.star InvolutiveStar.toStar instInvolutiveStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	—
mem_toNonUnitalStarSubalgebra 📖	mathematical	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Star.star	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalStarSubalgebra.instSetLike toNonUnitalStarSubalgebra NonUnitalSubalgebra instSetLike	—	—
starClosure_eq_adjoin 📖	mathematical	—	starClosure NonUnitalStarAlgebra.adjoin SetLike.coe NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring instSetLike	—	le_antisymm starClosure_le_iff NonUnitalStarAlgebra.subset_adjoin NonUnitalStarAlgebra.adjoin_le le_sup_left
starClosure_le 📖	mathematical	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalStarSubalgebra.toNonUnitalSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder starClosure	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff sup_le StarMemClass.star_mem NonUnitalStarSubalgebra.instStarMemClass mem_star_iff star_star
starClosure_le_iff 📖	mathematical	—	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Preorder.toLE PartialOrder.toPreorder NonUnitalStarSubalgebra.instPartialOrder starClosure NonUnitalSubalgebra instPartialOrder NonUnitalStarSubalgebra.toNonUnitalSubalgebra	—	LE.le.trans le_sup_left starClosure_le
starClosure_mono 📖	mathematical	—	Monotone NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalStarSubalgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid PartialOrder.toPreorder instPartialOrder NonUnitalStarSubalgebra.instPartialOrder starClosure	—	starClosure_le LE.le.trans le_sup_left
starClosure_toNonUnitalSubalgebra 📖	mathematical	—	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid starClosure NonUnitalSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra Star.star instInvolutiveStar	—	—
star_adjoin_comm 📖	mathematical	—	Star.star NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar instInvolutiveStar NonUnitalAlgebra.adjoin Set Set.star StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	NonUnitalAlgebra.adjoin_le NonUnitalAlgebra.subset_adjoin le_antisymm NonUnitalAlgebra.adjoin.congr_simp star_star star_mono
star_mem_star_iff 📖	mathematical	—	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Star.star InvolutiveStar.toStar instInvolutiveStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	star_star
star_mono 📖	mathematical	—	Monotone NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring PartialOrder.toPreorder instPartialOrder Star.star InvolutiveStar.toStar instInvolutiveStar	—	—
toNonUnitalStarSubalgebra_toNonUnitalSubalgebra 📖	mathematical	NonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike Star.star	NonUnitalStarSubalgebra.toNonUnitalSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring toNonUnitalStarSubalgebra	—	SetLike.coe_injective

StarAlgEquiv

Definitions

Name	Category	Theorems
ofInjective' 📖	CompOp	1 math math: ofInjective'_apply
ofLeftInverse' 📖	CompOp	2 math math: ofLeftInverse'_apply, ofLeftInverse'_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofInjective'_apply 📖	mathematical	DFunLike.coe	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgHom.range DFunLike.coe StarAlgEquiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring Distrib.toMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalStarSubalgebra.instModule StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass instFunLike ofInjective'	—	NonUnitalStarSubalgebra.instStarMemClass
ofLeftInverse'_apply 📖	mathematical	DFunLike.coe	NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgHom.range DFunLike.coe StarAlgEquiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring Distrib.toMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalStarSubalgebra.instModule StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass instFunLike ofLeftInverse'	—	NonUnitalStarSubalgebra.instStarMemClass
ofLeftInverse'_symm_apply 📖	mathematical	DFunLike.coe	DFunLike.coe StarAlgEquiv NonUnitalStarSubalgebra NonUnitalSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgHom.range Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalStarSubalgebra.toNonUnitalSemiring Distrib.toMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NonUnitalStarSubalgebra.instModule StarMemClass.instStar NonUnitalStarSubalgebra.instStarMemClass instFunLike symm ofLeftInverse'	—	NonUnitalStarSubalgebra.instStarMemClass

StarMemClass

Definitions

Name	Category	Theorems
instInvolutiveStar 📖	CompOp	—
instStarAddMonoid 📖	CompOp	—
instStarMul 📖	CompOp	—
instStarRing 📖	CompOp	1 math math: NonUnitalStarSubalgebra.unitization_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarModule 📖	mathematical	—	StarModule SetLike.instMembership instStar SetLike.smul	—	StarModule.star_smul

(root)

Definitions

Name	Category	Theorems
NonUnitalStarSubalgebra 📖	CompData	174 math math: range_cfcₙ_nnreal, NonUnitalSubalgebra.coe_starClosure, NonUnitalStarSubalgebra.mem_carrier, NonUnitalStarSubalgebra.topologicalClosure_map_le, NonUnitalStarSubalgebra.coe_zero, NonUnitalStarSubalgebra.ofClass_carrier, NonUnitalStarSubalgebra.mem_map, NonUnitalStarSubalgebra.instSMulMemClass, StarAlgEquiv.ofLeftInverse'_apply, cfcₙHom_apply_mem_elemental, NonUnitalStarAlgHom.coe_codRestrict, NonUnitalStarAlgebra.mem_bot, NonUnitalStarSubalgebra.centralizer_le, NonUnitalStarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, NonUnitalStarAlgebra.mem_sup_right, NonUnitalStarSubalgebra.topologicalClosure_minimal, NonUnitalStarAlgebra.coe_bot, NonUnitalStarAlgebra.mem_top, NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra, NonUnitalStarAlgebra.elemental.isClosedEmbedding_coe, NonUnitalStarSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar, NonUnitalStarSubalgebra.subsingleton_of_subsingleton, StarSubalgebra.mem_toNonUnitalStarSubalgebra, NonUnitalStarSubalgebra.coe_copy, NonUnitalStarSubalgebra.mem_comap, cfcₙHom_mem_elemental, NonUnitalStarSubalgebra.coe_neg, StarSubalgebra.toNonUnitalStarSubalgebra_injective, NonUnitalStarAlgebra.mem_sInf, NonUnitalSubalgebra.starClosure_le_iff, StarAlgebra.adjoin_nonUnitalStarSubalgebra, NonUnitalStarSubalgebra.instNonUnitalSubringClass, NonUnitalStarAlgHom.range_comp_le_range, NonUnitalStarAlgebra.instIsMulCommutative_adjoin, NonUnitalStarAlgHom.injective_codRestrict, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, NonUnitalStarAlgebra.coe_top, NonUnitalStarSubalgebra.coe_toNonUnitalSubring, NonUnitalStarAlgebra.coe_sInf, NonUnitalStarSubalgebra.val_inclusion, NonUnitalStarSubalgebra.instIsTopologicalSemiring, NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, range_cfcₙ, NonUnitalStarSubalgebra.map_mono, NonUnitalStarAlgebra.adjoin_le, cfcₙ_mem_elemental, NonUnitalStarSubalgebra.instIsTorsionFree, NonUnitalStarAlgebra.adjoin_mono, Unitization.starLift_range, NonUnitalStarSubalgebra.mem_toNonUnitalSubring, NonUnitalStarAlgebra.mem_iInf, NonUnitalStarSubalgebra.ext_iff, NonUnitalStarAlgebra.gc, NonUnitalStarAlgebra.subset_adjoin, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype, NonUnitalStarSubalgebra.range_val, NonUnitalSubalgebra.starClosure_mono, NonUnitalStarAlgebra.elemental.isClosed, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, NonUnitalStarSubalgebra.inclusion_mk, NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra, Unitization.inrRangeEquiv_apply_coe_snd, NonUnitalStarAlgebra.range_eq_top, NonUnitalStarSubalgebra.coe_centralizer, range_cfcₙ_eq_range_cfcₙHom, ContinuousMap.adjoin_id_eq_span_one_union, NonUnitalStarSubalgebra.topologicalClosure_mono, range_cfcₙHom_le, NonUnitalStarSubalgebra.iSupLift_inclusion, NonUnitalStarSubalgebra.mem_centralizer_iff, Unitization.inrRangeEquiv_apply_coe_fst, NonUnitalStarAlgebra.elemental.self_mem, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, NonUnitalStarAlgebra.star_subset_adjoin, NonUnitalStarAlgebra.mul_mem_sup, NonUnitalSubalgebra.starClosure_le, NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass, NonUnitalStarSubalgebra.prod_mono, NonUnitalStarAlgebra.mem_sup_left, NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgebra.elemental.le_centralizer_centralizer, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff, NonUnitalStarSubalgebra.iSupLift_of_mem, NonUnitalStarSubalgebra.prod_inf_prod, NonUnitalStarSubalgebra.instIsSemitopologicalRing, NonUnitalStarAlgebra.comap_top, NonUnitalStarAlgebra.elemental.star_self_mem, NonUnitalStarSubalgebra.coe_eq_zero, NonUnitalStarAlgebra.isMulCommutative_adjoin, NonUnitalStarAlgHom.mem_range_self, NonUnitalStarSubalgebra.le_topologicalClosure, NonUnitalStarAlgebra.coe_iInf, range_cfcₙ_subset, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, NonUnitalStarSubalgebra.mem_center_iff, NonUnitalStarSubalgebra.gc_map_comap, NonUnitalStarSubalgebra.coe_center, NonUnitalStarSubalgebra.instIsTopologicalRing, NonUnitalStarSubalgebra.inclusion_right, NonUnitalStarSubalgebra.coe_smul, range_cfcₙ_nnreal_subset, NonUnitalStarAlgebra.map_bot, NonUnitalStarSubalgebra.instSMulCommClass', NonUnitalStarSubalgebra.iSupLift_comp_inclusion, NonUnitalStarSubalgebra.map_injective, NonUnitalStarSubalgebra.coe_centralizer_centralizer, NonUnitalStarSubalgebra.coe_iSup_of_directed, NonUnitalStarAlgebra.mem_adjoin_of_mem, NonUnitalStarSubalgebra.toSubring_subtype, NonUnitalStarAlgHom.mem_equalizer, cfcₙAux_mem_range_inr, ContinuousMap.adjoin_id_eq_span_one_add, NonUnitalStarAlgebra.adjoin_le_iff, NonUnitalStarAlgebra.span_eq_toSubmodule, NonUnitalStarSubalgebra.instNoZeroDivisors, NonUnitalStarAlgHom.mem_range, NonUnitalStarAlgebra.coe_inf, NonUnitalStarAlgebra.map_sup, NonUnitalStarAlgHom.subtype_comp_codRestrict, NonUnitalStarAlgebra.adjoin_eq, NonUnitalStarSubalgebra.coe_mul, NonUnitalStarAlgebra.range_id, StarSubalgebra.one_mem_toNonUnitalStarSubalgebra, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, NonUnitalStarAlgebra.map_top, NonUnitalStarAlgebra.elemental.le_of_mem, NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra, NonUnitalStarAlgebra.star_self_mem_adjoin_singleton, NonUnitalStarAlgebra.elemental.le_iff_mem, NonUnitalStarSubalgebra.coe_add, NonUnitalStarSubalgebra.instIsSemitopologicalSemiring, NonUnitalStarSubalgebra.center_eq_top, StarAlgEquiv.ofInjective'_apply, NonUnitalStarSubalgebra.coe_prod, NonUnitalStarAlgebra.eq_top_iff, NonUnitalStarSubalgebra.instIsScalarTower, NonUnitalStarSubalgebra.inclusion_injective, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, NonUnitalStarAlgebra.self_mem_adjoin_singleton, NonUnitalStarAlgebra.map_inf, cfcₙ_apply_mem_elemental, Unitization.starLift_range_le, NonUnitalStarSubalgebra.map_le, NonUnitalStarSubalgebra.prod_top, ContinuousMapZero.elemental_eq_top, ContinuousMapZero.adjoin_id_dense, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, StarAlgEquiv.ofLeftInverse'_symm_apply, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, NonUnitalStarSubalgebra.coe_sub, NonUnitalStarSubalgebra.map_topologicalClosure_le, NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin, NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra, NonUnitalStarSubalgebra.instSMulCommClass, Unitization.inrRangeEquiv_symm_apply, NonUnitalStarSubalgebra.mem_prod, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalStarSubalgebra.iSupLift_mk, NonUnitalStarSubalgebra.toNonUnitalSubring_injective, NonUnitalStarSubalgebra.inclusion_self, NonUnitalSubalgebra.mem_starClosure, NonUnitalStarSubalgebra.instIsScalarTower', NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, NonUnitalStarSubalgebra.coe_comap, NonUnitalStarAlgebra.mem_inf, NonUnitalStarSubalgebra.inclusion_inclusion, NonUnitalStarSubalgebra.instStarMemClass, NonUnitalStarAlgebra.map_iInf, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra, NonUnitalStarAlgHom.coe_range, NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer, NonUnitalStarSubalgebra.isClosed_topologicalClosure
NonUnitalSubalgebra 📖	CompData	181 math math: NonUnitalSubalgebra.coe_starClosure, NonUnitalSubalgebra.center_eq_top, NonUnitalAlgebra.adjoin_le_algebra_adjoin, NonUnitalAlgebra.gc, NonUnitalSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul, NonUnitalSubalgebra.topologicalClosure_mono, NonUnitalAlgebra.adjoin_le, Subalgebra.mem_toNonUnitalSubalgebra, NonUnitalSubalgebra.instIsScalarTower', NonUnitalAlgHom.range_comp_le_range, NonUnitalAlgebra.coe_bot, NonUnitalAlgebra.span_eq_toSubmodule, NonUnitalAlgebra.mem_sup_left, NonUnitalAlgebra.coe_inf, NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra, NonUnitalAlgebra.elemental.isClosedEmbedding_coe, NonUnitalSubalgebra.topologicalClosure_minimal, NonUnitalSubalgebra.inclusion_mk, NonUnitalSubalgebra.topologicalClosure_map_le, NonUnitalAlgebra.sInf_toNonUnitalSubsemiring, NonUnitalAlgebra.adjoin_le_centralizer_centralizer, NonUnitalSubalgebra.inclusion_right, NonUnitalSubalgebra.toSubmodule_injective, NonUnitalSubalgebra.coe_toNonUnitalSubring, NonUnitalAlgebra.self_mem_adjoin_singleton, NonUnitalSubalgebra.prod_inf_prod, NonUnitalSubalgebra.ext_iff, NonUnitalAlgebra.mem_sup_right, NonUnitalSubalgebra.starClosure_le_iff, NonUnitalSubalgebra.prod_top, NonUnitalSubalgebra.instNonUnitalSubsemiringClass, NonUnitalAlgebra.mem_inf, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, NonUnitalSubalgebra.coe_toNonUnitalSubsemiring, NonUnitalSubalgebra.inclusion_self, NonUnitalSubalgebra.iSupLift_of_mem, NonUnitalAlgebra.instIsMulCommutative_adjoin, NonUnitalSubalgebra.mem_toNonUnitalSubsemiring, NonUnitalAlgebra.subset_adjoin, NonUnitalSubalgebra.iSupLift_comp_inclusion, NonUnitalSubalgebra.coe_copy, NonUnitalAlgebra.range_id, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective, NonUnitalAlgHom.mem_range, NonUnitalAlgebra.mem_iInf, NonUnitalSubalgebra.mem_map, NonUnitalAlgebra.mul_mem_sup, Subalgebra.toNonUnitalSubalgebra_mono, NonUnitalAlgHom.mem_range_self, NonUnitalSubalgebra.mem_star_iff, NonUnitalSubalgebra.inclusion_injective, NonUnitalAlgebra.adjoin_le_iff, NonUnitalAlgebra.toSubmodule_bot, NonUnitalSubalgebra.iSupLift_mk, Algebra.adjoin_nonUnitalSubalgebra_eq_span, NonUnitalSubalgebra.noZeroDivisors, NonUnitalAlgHom.injective_codRestrict, NonUnitalSubalgebra.coe_sub, NonUnitalSubalgebra.toNonUnitalSubring_injective, NonUnitalSubalgebra.toSubring_subtype, NonUnitalSubalgebra.coe_zero, NonUnitalAlgebra.top_toNonUnitalSubsemiring, NonUnitalSubalgebra.starClosure_mono, NonUnitalSubalgebra.iSupLift_inclusion, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra, NonUnitalAlgebra.elemental.isClosed, NonUnitalSubalgebra.instSMulCommClass, NonUnitalSubalgebra.map_le, NonUnitalSubalgebra.map_mono, NonUnitalSubalgebra.le_topologicalClosure, NonUnitalSubalgebra.mem_comap, NonUnitalSubalgebra.inclusion_inclusion, NonUnitalSubalgebra.coe_iSup_of_directed, NonUnitalAlgebra.map_sup, NonUnitalAlgebra.eq_top_iff, NonUnitalSubalgebra.starClosure_eq_adjoin, NonUnitalSubalgebra.mem_centralizer_iff, NonUnitalSubalgebra.coe_comap, NonUnitalAlgebra.coe_iInf, Unitization.lift_range, NonUnitalAlgebra.mem_top, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, NonUnitalAlgebra.elemental.le_of_mem, NonUnitalSubalgebra.centralizer_le, NonUnitalAlgHom.coe_range, NonUnitalSubalgebra.gc_map_comap, NonUnitalSubalgebra.mem_center_iff, NonUnitalSubalgebra.coe_map, NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_univ, NonUnitalSubalgebra.coe_star, NonUnitalSubalgebra.instSMulMemClass, Algebra.adjoin_nonUnitalSubalgebra, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff, NonUnitalSubalgebra.ofClass_carrier, NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, NonUnitalSubalgebra.instIsSemitopologicalSemiring, Subalgebra.toNonUnitalSubalgebra_injective, NonUnitalSubalgebra.instIsTopologicalRing, NonUnitalAlgebra.map_iInf, NonUnitalSubalgebra.instSMulCommClass', NonUnitalSubalgebra.isClosed_topologicalClosure, NonUnitalSubalgebra.mem_carrier, NonUnitalSubalgebra.map_topologicalClosure_le, NonUnitalSubalgebra.coe_centralizer, NonUnitalSubalgebra.coe_center, NonUnitalSubalgebra.star_mono, NonUnitalAlgebra.toSubmodule_eq_top, NonUnitalAlgebra.adjoin_empty, NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra, NonUnitalAlgebra.isMulCommutative_adjoin_singleton, NonUnitalSubalgebra.coe_prod, NonUnitalAlgebra.elemental.le_centralizer_centralizer, NonUnitalAlgebra.coe_top, NonUnitalAlgebra.map_top, NonUnitalAlgebra.to_subring_eq_top, NonUnitalAlgebra.toNonUnitalSubring_eq_top, Subalgebra.toNonUnitalSubalgebra_le_toNonUnitalSubalgebra, NonUnitalSubalgebra.toNonUnitalSubsemiring_injective, NonUnitalAlgebra.inf_toSubmodule, NonUnitalSubalgebra.instIsTorsionFree, NonUnitalSubalgebra.coe_smul, NonUnitalAlgebra.mem_sInf, NonUnitalAlgebra.comap_top, NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra, Unitization.lift_range_le, NonUnitalSubalgebra.instIsTopologicalSemiring, NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype, NonUnitalSubalgebra.coe_neg, NonUnitalAlgebra.map_bot, NonUnitalSubalgebra.instNonUnitalSubringClass, Submodule.coe_toNonUnitalSubalgebra, NonUnitalSubalgebra.instIsScalarTowerSubtypeMem, NonUnitalAlgebra.elemental.le_iff_mem, NonUnitalStarAlgebra.isMulCommutative_toNonUnitalSubalgebra, NonUnitalAlgebra.coe_sInf, NonUnitalSubalgebra.map_injective, NonUnitalSubalgebra.coe_inclusion, mem_nonUnitalSubalgebraOfNonUnitalSubsemiring, NonUnitalAlgebra.range_eq_top, NonUnitalSubalgebra.instIsSemitopologicalRing, NonUnitalAlgebra.elemental.self_mem, NonUnitalSubalgebra.mem_toSubmodule, NonUnitalAlgebra.top_toSubring, NonUnitalAlgebra.mem_bot, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, NonUnitalAlgebra.top_toSubmodule, NonUnitalAlgebra.isMulCommutative_adjoin, NonUnitalAlgebra.adjoin_eq, mem_nonUnitalSubalgebraOfNonUnitalSubring, NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, NonUnitalSubalgebra.coe_mul, NonUnitalSubalgebra.subsingleton_of_subsingleton, NonUnitalAlgebra.sInf_toSubmodule, NonUnitalAlgHom.mem_equalizer, NonUnitalAlgHom.coe_codRestrict, NonUnitalSubalgebra.coe_toSubmodule, NonUnitalAlgebra.toNonUnitalSubring_top, NonUnitalAlgebra.adjoin_union, NonUnitalAlgebra.mem_adjoin_of_mem, NonUnitalSubalgebra.mem_toNonUnitalSubring, NonUnitalSubalgebra.coe_eq_zero, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.inf_toNonUnitalSubsemiring, NonUnitalSubalgebra.mem_prod, NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top, NonUnitalSubalgebra.mem_starClosure, Subalgebra.one_mem_toNonUnitalSubalgebra, NonUnitalSubalgebra.coe_add, NonUnitalSubalgebra.prod_mono, NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, NonUnitalAlgebra.map_inf, NonUnitalSubalgebra.range_val, NonUnitalAlgebra.iInf_toSubmodule, NonUnitalAlgHom.subtype_comp_codRestrict, NonUnitalAlgebra.adjoin_mono, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra, Submodule.mem_toNonUnitalSubalgebra, NonUnitalSubalgebra.star_mem_star_iff, NonUnitalSubalgebra.star_adjoin_comm

---

← Back to Index