Documentation Verification Report

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`	`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`
`nonneg_of_mem_quasispectrum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Set` `Set.instMembership` `quasispectrum`	`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` `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`	`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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `quasispectrum`	—	`Set.eq_of_subset_of_subset` `quasispectrum.preimage_algebraMap` `Set.image_preimage_subset` `quasispectrum.of_algebraMap_mem` `rightInvOn`
`apply_mem` 📖	—	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `Set` `Set.instMembership` `quasispectrum`	—	—	`image`
`comp` 📖	—	`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`	—	`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` 📖	—	`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` 📖	—	`QuasispectrumRestricts` `Semifield.toCommSemiring` `Field.toSemifield` `quasispectrum`	—	—	`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`	—	—
`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` `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` 📖	—	`SpectrumRestricts` `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` 📖	—	`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` 📖	—	`SpectrumRestricts` `spectrum` `Semifield.toCommSemiring`	—	—	`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` `instRing` `instAlgebra` `NonUnitalRing.toNonUnitalSemiring` `Algebra.id` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `IsScalarTower.left` `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` `fst` `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` `Field.toSemifield` `NonUnitalRing.toNonUnitalSemiring` `Module.toDistribMulAction` `CommSemiring.toSemiring` `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	—	`fst` `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	—	`fst` `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` `snd` `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` `snd`	—	—
`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	9 math math: `isQuasiregular_iff`, `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	15 math math: `IsSelfAdjoint.quasispectrumRestricts`, `quasispectrumRestricts_iff_spectrumRestricts_inr'`, `QuasispectrumRestricts.nnreal_iff`, `quasispectrumRestricts_iff`, `isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts`, `nonneg_iff_isSelfAdjoint_and_spectrumRestricts`, `QuasispectrumRestricts.real_iff`, `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`, `QuasispectrumRestricts.of_subset_range_algebraMap`, `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	15 math math: `SpectrumRestricts.nnreal_of_nonneg`, `spectrumRestricts_iff`, `quasispectrumRestricts_iff_spectrumRestricts_inr'`, `SpectrumRestricts.nnreal_iff`, `SpectrumRestricts.mul_comm_iff`, `IsSelfAdjoint.spectrumRestricts`, `SpectrumRestricts.real_iff`, `IsSelfAdjoint.sq_spectrumRestricts`, `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`
`quasispectrum` 📖	CompOp	77 math math: `cfcₙ_def`, `norm_cfcₙHom`, `quasispectrum_eq_spectrum_union`, `spectrum_subset_quasispectrum`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `QuasispectrumRestricts.compactSpace`, `isClosedEmbedding_cfcₙAux`, `quasispectrumRestricts_iff`, `QuasispectrumRestricts.rightInvOn`, `NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum`, `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`, `range_cfcₙHom`, `Unitization.quasispectrum_inr_eq`, `quasispectrum.zero_mem`, `continuousOn_cfcₙ`, `quasispectrum.isCompact`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `QuasispectrumRestricts.subset_preimage`, `Commute.cfcₙHom`, `NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum`, `range_cfcₙ_eq_range_cfcₙHom`, `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`, `cfcₙHom_le_iff`, `NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙHom_map_quasispectrum`, `quasispectrum.algebraMap_mem_iff`, `QuasispectrumRestricts.algebraMap_image`, `NonUnitalAlgHom.quasispectrum_apply_subset'`, `spec_cfcₙAux`, `upperHemicontinuous_quasispectrum_nnreal`, `nnnorm_cfcₙHom`, `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`, `continuousOn_cfcₙ_nnreal`, `cfcₙHom_continuous`, `Unitization.quasispectrum_eq_spectrum_inr'`, `cfcₙ_apply_pi`, `continuousOn_cfcₙ_setProd`, `NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum`, `quasispectrum.not_isUnit_mem`, `cfcₙL_apply`, `quasispectrum_eq_spectrum_union_zero`, `IsIdempotentElem.quasispectrum_subset`, `quasispectrum.preimage_algebraMap`, `instFactMemSetQuasispectrumOfNat`, `Prod.quasispectrum_eq`, `quasispectrum.instCompactSpaceNNReal`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `Unitization.quasispectrum_eq_spectrum_inr`, `continuousOn_cfcₙ_nnreal_setProd`, `cfcₙHom_nonneg_iff`, `quasispectrum.instCompactSpace`

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` `NonUnitalRing.toNonUnitalSemiring` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `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` `Field.toSemifield` `NonUnitalRing.toNonUnitalSemiring` `Module.toDistribMulAction` `CommSemiring.toSemiring` `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`	`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	35 math math: `cfcₙ_def`, `norm_cfcₙHom`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `isClosedEmbedding_cfcₙAux`, `coe_zero`, `cfcₙ_eq_cfcₙL_mkD`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `range_cfcₙHom`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `Commute.cfcₙHom`, `range_cfcₙ_eq_range_cfcₙHom`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `cfcₙHom_eq_cfcₙ_extend`, `cfcₙHom_map_quasispectrum`, `spec_cfcₙAux`, `nnnorm_cfcₙHom`, `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`, `cfcₙ_eq_cfcₙL`, `cfcₙL_apply`, `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`	`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`	—	`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` 📖	—	`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`
`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