Spectrum

📁 Source: Mathlib/Analysis/Complex/Spectrum.lean

Statistics

Metric	Count
Definitions	0
Theorems real_iff, real_iff	2
Total	2

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
real_iff 📖	mathematical	—	QuasispectrumRestricts Real Complex Real.instCommSemiring Complex.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM Complex.ofReal Complex.re	—	IsScalarTower.complexToReal IsScalarTower.left quasispectrumRestricts_iff_spectrumRestricts_inr Unitization.quasispectrum_eq_spectrum_inr' SpectrumRestricts.real_iff

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
real_iff 📖	mathematical	—	SpectrumRestricts Real Complex Field.toSemifield Real.instField Complex.instField Algebra.complexToReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM Complex.ofReal Complex.re	—	algebraMap_image IsScalarTower.complexToReal IsScalarTower.left of_subset_range_algebraMap Complex.ofReal_re

---

← Back to Index