Quasispectrum

📁 Source: Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

Statistics

Metric	Count
Definitions IsQuasiregular, NonnegSpectrumClass, PreQuasiregular, equiv, instMonoid, instMul, instOne, val, QuasispectrumRestricts, SpectrumRestricts, unitsFstOne, unitsFstOne_mulEquiv_quasiregular, quasispectrum, instZero	14
Theorems isUnit_one_add, map, quasispectrum_apply_subset, quasispectrum_apply_subset', iff_spectrum_nonneg, nonneg_of_mem_quasispectrum, of_spectrum_nonneg, quasispectrum_nonneg_of_nonneg, add_inv_add_mul_eq_zero, equiv_apply_val, equiv_symm_apply, inv_add_add_mul_eq_zero, val_mul, val_one, algebraMap_image, apply_mem, comp, image, left_inv, map_zero, mul_comm, mul_comm_iff, of_quasispectrum_eq, of_subset_range_algebraMap, rightInvOn, subset_preimage, algebraMap_image, apply_mem, image, mul_comm, mul_comm_iff, of_rightInvOn, of_spectrum_eq, of_subset_range_algebraMap, rightInvOn, subset_preimage, isQuasiregular_inr_iff, mem_spectrum_inr_of_not_isUnit, mem_unitsFstOne, quasispectrum_eq_spectrum_inr, quasispectrum_eq_spectrum_inr', quasispectrum_inr_eq, unitsFstOne_val_inv_val_fst, unitsFstOne_val_val_fst, val_inv_unitsFstOne_mulEquiv_quasiregular_apply, val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_unitsFstOne_mulEquiv_quasiregular_apply, val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, zero_mem_spectrum_inr, isQuasiregular_iff, isQuasiregular_iff', isQuasiregular_iff_isUnit, isQuasiregular_iff_isUnit', isQuasiregular_zero, mem_quasispectrum_iff, algebraMap_mem, algebraMap_mem_iff, coe_zero, mem_of_not_quasiregular, mul_comm, nonempty, not_isUnit_mem, of_algebraMap_mem, preimage_algebraMap, zero_mem, quasispectrumRestricts_iff, quasispectrumRestricts_iff_spectrumRestricts, quasispectrumRestricts_iff_spectrumRestricts_inr, quasispectrumRestricts_iff_spectrumRestricts_inr', quasispectrum_eq_spectrum_union, quasispectrum_eq_spectrum_union_zero, spectrumRestricts_iff, spectrum_nonneg_of_nonneg, spectrum_subset_quasispectrum	74
Total	88

IsQuasiregular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_one_add 📖	mathematical	IsQuasiregular Semiring.toNonUnitalSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	isQuasiregular_iff mul_add Distrib.leftDistribClass mul_one add_mul Distrib.rightDistribClass one_mul Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.const_add_term add_zero
map 📖	mathematical	IsQuasiregular	IsQuasiregular DFunLike.coe	—	isQuasiregular_iff map_add AddMonoidHomClass.toAddHomClass NonUnitalRingHomClass.toAddMonoidHomClass map_mul NonUnitalRingHomClass.toMulHomClass map_zero AddMonoidHomClass.toZeroHomClass

NonUnitalAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasispectrum_apply_subset 📖	mathematical	—	Set Set.instHasSubset quasispectrum CommRing.toCommSemiring DFunLike.coe	—	quasispectrum_apply_subset' IsScalarTower.left
quasispectrum_apply_subset' 📖	mathematical	—	Set Set.instHasSubset quasispectrum DFunLike.coe	—	Set.compl_subset_compl Units.smul_def smul_one_smul map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass IsQuasiregular.map NonUnitalAlgHomClass.toNonUnitalRingHomClass

NonnegSpectrumClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_spectrum_nonneg 📖	mathematical	—	NonnegSpectrumClass Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	quasispectrum_eq_spectrum_union_zero Set.union_singleton instReflLe
nonneg_of_mem_quasispectrum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set Set.instMembership quasispectrum	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	quasispectrum_nonneg_of_nonneg
of_spectrum_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	NonnegSpectrumClass Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring	—	iff_spectrum_nonneg
quasispectrum_nonneg_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set Set.instMembership quasispectrum	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—

PreQuasiregular

Definitions

Name	Category	Theorems
equiv 📖	CompOp	7 math math: equiv_symm_apply, equiv_apply_val, isQuasiregular_iff', Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply
instMonoid 📖	CompOp	7 math math: add_inv_add_mul_eq_zero, inv_add_add_mul_eq_zero, isQuasiregular_iff', Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply
instMul 📖	CompOp	1 math math: val_mul
instOne 📖	CompOp	1 math math: val_one
val 📖	CompOp	6 math math: equiv_symm_apply, add_inv_add_mul_eq_zero, inv_add_add_mul_eq_zero, equiv_apply_val, val_mul, val_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_inv_add_mul_eq_zero 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring val Units.val PreQuasiregular instMonoid Units Units.instInv Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Units.inv_mul
equiv_apply_val 📖	mathematical	—	val DFunLike.coe Equiv PreQuasiregular EquivLike.toFunLike Equiv.instEquivLike equiv	—	—
equiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv PreQuasiregular EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv val	—	—
inv_add_add_mul_eq_zero 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring val Units.val PreQuasiregular instMonoid Units Units.instInv Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Units.mul_inv
val_mul 📖	mathematical	—	val PreQuasiregular instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Distrib.toMul	—	—
val_one 📖	mathematical	—	val PreQuasiregular instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	—

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_image 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap quasispectrum	—	Set.eq_of_subset_of_subset quasispectrum.preimage_algebraMap Set.image_preimage_subset quasispectrum.of_algebraMap_mem rightInvOn
apply_mem 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield Set Set.instMembership quasispectrum	Set Set.instMembership quasispectrum Semifield.toCommSemiring	—	image
comp 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	—	IsScalarTower.algebraMap_eq Set.RightInvOn.comp rightInvOn apply_mem Function.LeftInverse.comp left_inv
image 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	Set.image quasispectrum Semifield.toCommSemiring Field.toSemifield	—	algebraMap_image Set.image_image Set.image_congr left_inv Set.image_id'
left_inv 📖	mathematical	QuasispectrumRestricts	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
map_zero 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	left_inv map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
mul_comm 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	mul_comm_iff
mul_comm_iff 📖	mathematical	—	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	quasispectrum.mul_comm
of_quasispectrum_eq 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield quasispectrum	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	—	rightInvOn left_inv
of_subset_range_algebraMap 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Set Set.instHasSubset quasispectrum Set.range	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	—	—
rightInvOn 📖	mathematical	QuasispectrumRestricts	Set.RightInvOn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap quasispectrum	—	—
subset_preimage 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield	Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield Set.preimage	—	Set.subset_preimage_image image

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_image 📖	mathematical	SpectrumRestricts	Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap spectrum	—	Set.eq_of_subset_of_subset spectrum.preimage_algebraMap Set.image_preimage_subset spectrum.of_algebraMap_mem rightInvOn
apply_mem 📖	mathematical	SpectrumRestricts Set Set.instMembership spectrum Semifield.toCommSemiring	Set Set.instMembership spectrum Semifield.toCommSemiring	—	image
image 📖	mathematical	SpectrumRestricts	Set.image spectrum Semifield.toCommSemiring	—	algebraMap_image Set.image_image Set.image_congr QuasispectrumRestricts.left_inv Set.image_id'
mul_comm 📖	mathematical	SpectrumRestricts Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	SpectrumRestricts Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	mul_comm_iff
mul_comm_iff 📖	mathematical	—	SpectrumRestricts Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	QuasispectrumRestricts.mul_comm_iff IsScalarTower.right Algebra.to_smulCommClass
of_rightInvOn 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Set.RightInvOn spectrum	SpectrumRestricts	—	mem_quasispectrum_iff IsDomain.toNontrivial instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass
of_spectrum_eq 📖	mathematical	SpectrumRestricts spectrum Semifield.toCommSemiring	SpectrumRestricts	—	quasispectrum_eq_spectrum_union_zero QuasispectrumRestricts.rightInvOn QuasispectrumRestricts.left_inv
of_subset_range_algebraMap 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Set Set.instHasSubset spectrum Set.range	SpectrumRestricts	—	mem_quasispectrum_iff IsDomain.toNontrivial instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass
rightInvOn 📖	mathematical	SpectrumRestricts	Set.RightInvOn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap spectrum	—	Set.RightInvOn.mono QuasispectrumRestricts.rightInvOn spectrum_subset_quasispectrum
subset_preimage 📖	mathematical	SpectrumRestricts	Set Set.instHasSubset spectrum Semifield.toCommSemiring Set.preimage	—	Set.subset_preimage_image image

Unitization

Definitions

Name	Category	Theorems
unitsFstOne 📖	CompOp	7 math math: val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_inv_unitsFstOne_mulEquiv_quasiregular_apply, val_unitsFstOne_mulEquiv_quasiregular_apply, unitsFstOne_val_val_fst, mem_unitsFstOne, unitsFstOne_val_inv_val_fst
unitsFstOne_mulEquiv_quasiregular 📖	CompOp	4 math math: val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_inv_unitsFstOne_mulEquiv_quasiregular_apply, val_unitsFstOne_mulEquiv_quasiregular_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasiregular_inr_iff 📖	mathematical	—	IsQuasiregular Unitization Semiring.toNonUnitalSemiring instSemiring NonUnitalRing.toNonUnitalSemiring inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	isQuasiregular_iff CanLift.prf instCanLift IsScalarTower.left add_zero MulZeroClass.zero_mul inr_injective inr_add inr_mul IsQuasiregular.map NonUnitalAlgHomClass.toNonUnitalRingHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass
mem_spectrum_inr_of_not_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Set Set.instMembership spectrum Unitization CommRing.toCommSemiring instRing instAlgebra NonUnitalRing.toNonUnitalSemiring Algebra.id Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.left map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AlgHom.commutes sub_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass
mem_unitsFstOne 📖	mathematical	—	Units Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne toProd Units.val AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—
quasispectrum_eq_spectrum_inr 📖	mathematical	—	quasispectrum CommRing.toCommSemiring spectrum Unitization instRing instAlgebra NonUnitalRing.toNonUnitalSemiring Algebra.id Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Set.ext IsScalarTower.left mem_spectrum_inr_of_not_isUnit Set.union_eq_left quasispectrum_eq_spectrum_union not_iff_not Units.smul_def inr_smul inr_neg isQuasiregular_inr_iff
quasispectrum_eq_spectrum_inr' 📖	mathematical	—	quasispectrum Semifield.toCommSemiring spectrum Unitization instRing Field.toCommRing instAlgebra CommRing.toCommSemiring NonUnitalRing.toNonUnitalSemiring Module.toDistribMulAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Set.ext Set.singleton_subset_iff zero_mem_spectrum_inr IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Set.union_eq_self_of_subset_right quasispectrum_eq_spectrum_union_zero not_iff_not Units.smul_def inr_smul inr_neg isQuasiregular_inr_iff
quasispectrum_inr_eq 📖	mathematical	—	quasispectrum Unitization Semifield.toCommSemiring Ring.toNonUnitalRing instRing Field.toCommRing instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalRing.toNonUnitalNonAssocRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	quasispectrum_eq_spectrum_union_zero quasispectrum_eq_spectrum_inr' Set.union_singleton zero_mem_spectrum_inr IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
unitsFstOne_val_inv_val_fst 📖	mathematical	—	toProd Units.val Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Units Units.instInv Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	mem_unitsFstOne
unitsFstOne_val_val_fst 📖	mathematical	—	toProd Units.val Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	mem_unitsFstOne
val_inv_unitsFstOne_mulEquiv_quasiregular_apply 📖	mathematical	—	Units.val PreQuasiregular PreQuasiregular.instMonoid Units Units.instInv DFunLike.coe MulEquiv Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitsFstOne_mulEquiv_quasiregular Equiv Equiv.instEquivLike PreQuasiregular.equiv toProd Subgroup.inv	—	—
val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📖	mathematical	—	Units.val Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Units Units.instInv Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne DFunLike.coe MulEquiv PreQuasiregular PreQuasiregular.instMonoid Units.instMul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitsFstOne_mulEquiv_quasiregular instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass inr Equiv Equiv.instEquivLike Equiv.symm PreQuasiregular.equiv	—	—
val_unitsFstOne_mulEquiv_quasiregular_apply 📖	mathematical	—	Units.val PreQuasiregular PreQuasiregular.instMonoid DFunLike.coe MulEquiv Units Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitsFstOne_mulEquiv_quasiregular Equiv Equiv.instEquivLike PreQuasiregular.equiv toProd	—	—
val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📖	mathematical	—	Units.val Unitization instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitsFstOne DFunLike.coe MulEquiv PreQuasiregular PreQuasiregular.instMonoid Units.instMul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitsFstOne_mulEquiv_quasiregular instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass inr Equiv Equiv.instEquivLike Equiv.symm PreQuasiregular.equiv	—	—
zero_mem_spectrum_inr 📖	mathematical	—	Set Set.instMembership spectrum Unitization instRing instAlgebra CommRing.toCommSemiring NonUnitalRing.toNonUnitalSemiring Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	spectrum.zero_mem_iff MulZeroClass.zero_mul NeZero.one Units.mul_inv

(root)

Definitions

Name	Category	Theorems
IsQuasiregular 📖	MathDef	10 math math: isQuasiregular_iff, IsQuasiregular.map, Unitization.isQuasiregular_inr_iff, quasispectrum.mem_iff_of_isUnit, isQuasiregular_iff', isQuasiregular_iff_isUnit, isQuasiregular_zero, isQuasiregular_prod_iff, isQuasiregular_iff_isUnit', isQuasiregular_pi_iff
NonnegSpectrumClass 📖	CompData	8 math math: CStarAlgebra.instNonnegSpectrumClassComplexNonUnital, CStarAlgebra.instNonnegSpectrumClass, Matrix.instNonnegSpectrumClass, ContinuousLinearMap.instNonnegSpectrumClassRealId, CStarAlgebra.instNonnegSpectrumClass', NonnegSpectrumClass.of_spectrum_nonneg, CStarAlgebra.instNonnegSpectrumClassComplexUnital, NonnegSpectrumClass.iff_spectrum_nonneg
PreQuasiregular 📖	CompData	11 math math: PreQuasiregular.equiv_symm_apply, PreQuasiregular.add_inv_add_mul_eq_zero, PreQuasiregular.inv_add_add_mul_eq_zero, PreQuasiregular.equiv_apply_val, isQuasiregular_iff', Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, PreQuasiregular.val_mul, PreQuasiregular.val_one, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply
QuasispectrumRestricts 📖	CompData	17 math math: QuasispectrumRestricts.of_quasispectrum_eq, IsSelfAdjoint.quasispectrumRestricts, quasispectrumRestricts_iff_spectrumRestricts_inr', QuasispectrumRestricts.nnreal_iff, quasispectrumRestricts_iff, CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, QuasispectrumRestricts.mul_comm, QuasispectrumRestricts.real_iff, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, QuasispectrumRestricts.of_subset_range_algebraMap, QuasispectrumRestricts.comp, quasispectrumRestricts_iff_spectrumRestricts_inr, QuasispectrumRestricts.nnreal_of_nonneg, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, quasispectrumRestricts_iff_spectrumRestricts, CStarAlgebra.nonneg_TFAE, QuasispectrumRestricts.mul_comm_iff
SpectrumRestricts 📖	MathDef	19 math math: SpectrumRestricts.nnreal_of_nonneg, SpectrumRestricts.of_spectrum_eq, spectrumRestricts_iff, quasispectrumRestricts_iff_spectrumRestricts_inr', SpectrumRestricts.nnreal_iff, SpectrumRestricts.smul_of_nonneg, SpectrumRestricts.mul_comm_iff, IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.real_iff, IsSelfAdjoint.sq_spectrumRestricts, SpectrumRestricts.mul_comm, SpectrumRestricts.of_subset_range_algebraMap, quasispectrumRestricts_iff_spectrumRestricts_inr, ContinuousLinearMap.IsPositive.spectrumRestricts, SpectrumRestricts.of_rightInvOn, quasispectrumRestricts_iff_spectrumRestricts, SpectrumRestricts.nnreal_iff_spectralRadius_le, SpectrumRestricts.nnreal_iff_nnnorm, SpectrumRestricts.nnreal_add
quasispectrum 📖	CompOp	115 math math: cfcₙ_def, cfcₙL_integral, norm_cfcₙHom, cfcₙHom_mono, quasispectrum_eq_spectrum_union, quasispectrum_imaginaryPart, spectrum_subset_quasispectrum, quasispectrum.algebraMap_mem, NonUnitalIsometricContinuousFunctionalCalculus.isometric, cfcₙHom_apply_mem_elemental, cfcₙHom_of_cfcHom_injective, quasispectrum.of_algebraMap_mem, QuasispectrumRestricts.compactSpace, isClosedEmbedding_cfcₙAux, quasispectrumRestricts_iff, QuasispectrumRestricts.rightInvOn, IsGreatest.nnnorm_cfcₙ, QuasispectrumRestricts.nonUnitalStarAlgHom_id, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, cfcₙHom_mem_elemental, quasispectrum.coe_zero, CFC.quasispectrum_zero_eq, cfcₙ_eq_cfcₙL_mkD, quasispectrum.mem_iff_of_isUnit, Pi.quasispectrum_eq, quasispectrum.nonempty, cfcₙ_apply_mkD, cfcₙHom_id, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, range_cfcₙHom, Unitization.quasispectrum_inr_eq, IsGreatest.norm_cfcₙ, NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding, cfcₙHom_integral, quasispectrum.zero_mem, continuousOn_cfcₙ, quasispectrum.isCompact, cfcₙAux_id, IsGreatest.nnnorm_cfcₙ_nnreal, isometry_cfcₙHom, cfcₙHom_predicate, quasispectrum_imaginaryPart', cfcₙHom_comp, QuasispectrumRestricts.subset_preimage, Commute.cfcₙHom, QuasispectrumRestricts.continuous_nonUnitalStarAlgHom, QuasispectrumRestricts.apply_mem, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum, range_cfcₙ_eq_range_cfcₙHom, range_cfcₙHom_le, NonUnitalAlgHom.quasispectrum_apply_subset, inr_comp_cfcₙHom_eq_cfcₙAux, quasispectrum.mem_of_not_quasiregular, mem_quasispectrum_iff, upperHemicontinuous_quasispectrum, lipschitzOnWith_cfcₙ_fun, cfcₙHom_isClosedEmbedding, isIdempotentElem_iff_quasispectrum_subset, cfcₙHom_le_iff, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, cfcₙHom_eq_cfcₙ_extend, cfcₙAux_injective, QuasispectrumRestricts.nonUnitalStarAlgHom_injective, cfcₙHom_map_quasispectrum, quasispectrum.algebraMap_mem_iff, quasispectrum_realPart, cfcₙ_eq_cfcₙ_iff_eqOn, QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom, QuasispectrumRestricts.algebraMap_image, NonUnitalAlgHom.quasispectrum_apply_subset', spec_cfcₙAux, cfcₙHom_injective, upperHemicontinuous_quasispectrum_nnreal, nnnorm_cfcₙHom, continuous_cfcₙHom_of_cfcHom, isClosedEmbedding_cfcₙHom_of_cfcHom, IsSelfAdjoint.commute_cfcₙHom, QuasispectrumRestricts.nonUnitalStarAlgHom_apply, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate, CFC.quasispectrum_abs, cfcₙAux_mem_range_inr, QuasispectrumRestricts.image, NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum, quasispectrum.mul_comm, quasispectrum.isCompact_nnreal, isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint, continuousOn_cfcₙ_nnreal, cfcₙHom_continuous, Unitization.quasispectrum_eq_spectrum_inr', IsIdempotentElem.finite_quasispectrum, cfcₙ_apply_pi, continuousOn_cfcₙ_setProd, NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum, quasispectrum.not_isUnit_mem, quasispectrum_realPart', continuous_cfcₙAux, cfcₙ_eq_cfcₙL, cfcₙL_apply, quasispectrum_eq_spectrum_union_zero, IsIdempotentElem.quasispectrum_subset, quasispectrum.preimage_algebraMap, instFactMemSetQuasispectrumOfNat, cfcₙL_integrable, Prod.quasispectrum_eq, quasispectrum.instCompactSpaceNNReal, cfcₙHom_of_cfcHom_map_quasispectrum, eqOn_of_cfcₙ_eq_cfcₙ, Unitization.quasispectrum_eq_spectrum_inr, cfcₙHomSuperset_apply, cfcₙ_apply, cfcₙ_map_quasispectrum, continuousOn_cfcₙ_nnreal_setProd, cfcₙHom_nonneg_iff, quasispectrum.instCompactSpace, isStarProjection_iff_quasispectrum_subset_and_isStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasiregular_iff 📖	mathematical	—	IsQuasiregular Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	PreQuasiregular.inv_add_add_mul_eq_zero PreQuasiregular.add_inv_add_mul_eq_zero Equiv.injective
isQuasiregular_iff' 📖	mathematical	—	IsQuasiregular IsUnit PreQuasiregular PreQuasiregular.instMonoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike PreQuasiregular.equiv	—	Equiv.injective Equiv.apply_symm_apply
isQuasiregular_iff_isUnit 📖	mathematical	—	IsQuasiregular Semiring.toNonUnitalSemiring Ring.toSemiring IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsQuasiregular.isUnit_one_add isQuasiregular_iff IsUnit.mul_val_inv sub_eq_add_neg mul_add Distrib.leftDistribClass mul_neg mul_one add_mul Distrib.rightDistribClass one_mul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg sub_self sub_add_cancel IsUnit.val_inv_mul neg_mul
isQuasiregular_iff_isUnit' 📖	mathematical	—	IsQuasiregular IsUnit Unitization Unitization.instMonoid CommSemiring.toCommMonoid Module.toDistribMulAction CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Unitization.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Unitization.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Unitization.inr	—	Units.isUnit add_zero zero_add Equiv.symm_apply_apply
isQuasiregular_zero 📖	mathematical	—	IsQuasiregular Nat.instNonUnitalSemiring	—	—
mem_quasispectrum_iff 📖	mathematical	—	Set Set.instMembership quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring spectrum	—	quasispectrum_eq_spectrum_union_zero Set.union_singleton
quasispectrumRestricts_iff 📖	mathematical	—	QuasispectrumRestricts Set.RightInvOn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap quasispectrum	—	—
quasispectrumRestricts_iff_spectrumRestricts 📖	mathematical	—	QuasispectrumRestricts Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring SpectrumRestricts	—	—
quasispectrumRestricts_iff_spectrumRestricts_inr 📖	mathematical	—	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield SpectrumRestricts Unitization Unitization.instRing Field.toCommRing Unitization.instAlgebra CommRing.toCommSemiring NonUnitalRing.toNonUnitalSemiring Module.toDistribMulAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.left quasispectrumRestricts_iff spectrumRestricts_iff Unitization.quasispectrum_eq_spectrum_inr'
quasispectrumRestricts_iff_spectrumRestricts_inr' 📖	mathematical	—	QuasispectrumRestricts Semifield.toCommSemiring SpectrumRestricts Unitization Unitization.instRing Field.toCommRing Unitization.instAlgebra CommRing.toCommSemiring NonUnitalRing.toNonUnitalSemiring Module.toDistribMulAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Unitization.quasispectrum_inr_eq
quasispectrum_eq_spectrum_union 📖	mathematical	—	quasispectrum Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring Set Set.instUnion spectrum setOf IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	Set.ext quasispectrum.eq_1 not_iff_not isQuasiregular_iff_isUnit sub_eq_add_neg Algebra.algebraMap_eq_smul_one IsUnit.smul_sub_iff_sub_inv_smul Units.instIsScalarTower IsScalarTower.right Units.smulCommClass_left Algebra.to_smulCommClass
quasispectrum_eq_spectrum_union_zero 📖	mathematical	—	quasispectrum Semifield.toCommSemiring Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring Set Set.instUnion spectrum Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	quasispectrum_eq_spectrum_union
spectrumRestricts_iff 📖	mathematical	—	SpectrumRestricts Set.RightInvOn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap spectrum	—	SpectrumRestricts.rightInvOn QuasispectrumRestricts.left_inv SpectrumRestricts.of_rightInvOn
spectrum_nonneg_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set Set.instMembership spectrum	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg spectrum_subset_quasispectrum
spectrum_subset_quasispectrum 📖	mathematical	—	Set Set.instHasSubset spectrum quasispectrum Ring.toNonUnitalRing Algebra.toModule Ring.toSemiring	—	Set.subset_union_left quasispectrum_eq_spectrum_union

quasispectrum

Definitions

Name	Category	Theorems
instZero 📖	CompOp	53 math math: cfcₙ_def, cfcₙL_integral, norm_cfcₙHom, cfcₙHom_mono, NonUnitalIsometricContinuousFunctionalCalculus.isometric, cfcₙHom_apply_mem_elemental, cfcₙHom_of_cfcHom_injective, isClosedEmbedding_cfcₙAux, QuasispectrumRestricts.nonUnitalStarAlgHom_id, cfcₙHom_mem_elemental, coe_zero, cfcₙ_eq_cfcₙL_mkD, cfcₙ_apply_mkD, cfcₙHom_id, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, range_cfcₙHom, NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding, cfcₙHom_integral, cfcₙAux_id, isometry_cfcₙHom, cfcₙHom_predicate, cfcₙHom_comp, Commute.cfcₙHom, QuasispectrumRestricts.continuous_nonUnitalStarAlgHom, range_cfcₙ_eq_range_cfcₙHom, range_cfcₙHom_le, inr_comp_cfcₙHom_eq_cfcₙAux, cfcₙHom_isClosedEmbedding, cfcₙHom_le_iff, cfcₙHom_eq_cfcₙ_extend, cfcₙAux_injective, QuasispectrumRestricts.nonUnitalStarAlgHom_injective, cfcₙHom_map_quasispectrum, QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom, spec_cfcₙAux, cfcₙHom_injective, nnnorm_cfcₙHom, continuous_cfcₙHom_of_cfcHom, isClosedEmbedding_cfcₙHom_of_cfcHom, IsSelfAdjoint.commute_cfcₙHom, QuasispectrumRestricts.nonUnitalStarAlgHom_apply, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate, cfcₙAux_mem_range_inr, cfcₙHom_continuous, cfcₙ_apply_pi, continuous_cfcₙAux, cfcₙ_eq_cfcₙL, cfcₙL_apply, cfcₙL_integrable, cfcₙHom_of_cfcHom_map_quasispectrum, cfcₙHomSuperset_apply, cfcₙ_apply, cfcₙHom_nonneg_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_mem 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	algebraMap_mem_iff
algebraMap_mem_iff 📖	mathematical	—	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr' Unitization.instIsScalarTower IsScalarTower.right
coe_zero 📖	mathematical	—	Set Set.instMembership quasispectrum Set.Elem instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
mem_of_not_quasiregular 📖	mathematical	IsQuasiregular NonUnitalRing.toNonUnitalSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Units.instInv	Set Set.instMembership quasispectrum Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	IsUnit.unit_of_val_units
mul_comm 📖	mathematical	—	quasispectrum CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Set.inter_union_compl IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr Unitization.inr_mul Set.inter_comm spectrum.setOf_isUnit_inter_mul_comm Set.inter_eq_right not_isUnit_mem
nonempty 📖	mathematical	—	Set.Nonempty quasispectrum	—	Set.nonempty_of_mem zero_mem
not_isUnit_mem 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	Set Set.instMembership quasispectrum	—	—
of_algebraMap_mem 📖	mathematical	Set Set.instMembership quasispectrum Semifield.toCommSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	Set Set.instMembership quasispectrum Semifield.toCommSemiring	—	algebraMap_mem_iff
preimage_algebraMap 📖	mathematical	—	Set.preimage DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap quasispectrum	—	Set.ext algebraMap_mem_iff
zero_mem 📖	mathematical	—	Set Set.instMembership quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	not_isUnit_mem NeZero.one

---

← Back to Index