Loogle!

Result

Found 439 declarations mentioning spectrum. Of these, only the first 200 are shown.

• spectrum 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) : Set R
• spectrum.of_subsingleton 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : A) : spectrum R a = ∅
• spectrum.isUnit_of_zero_notMem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∉ spectrum R a → IsUnit a
• spectrum.not_isUnit_of_zero_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∈ spectrum R a → ¬IsUnit a
• spectrum.zero_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : ¬IsUnit a → 0 ∈ spectrum R a
• spectrum.zero_notMem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : IsUnit a → 0 ∉ spectrum R a
• spectrum.zero_mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∈ spectrum R a ↔ ¬IsUnit a
• spectrum.zero_notMem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∉ spectrum R a ↔ IsUnit a
• spectrum.resolvent_zero_of_mem_spectrum 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} (hr : r ∈ spectrum R a) : resolvent a r = 0
• Units.zero_notMem_spectrum 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : Aˣ) : 0 ∉ spectrum R ↑a
• spectrum.mem_spectrum_iff_resolvent_zero 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Nontrivial A] {r : R} {a : A} : r ∈ spectrum R a ↔ resolvent a r = 0
• spectrum.ne_zero_of_mem_of_unit 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : Aˣ} {r : R} (hr : r ∈ spectrum R ↑a) : r ≠ 0
• spectrum.subset_singleton_zero_compl 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} (ha : IsUnit a) : spectrum R a ⊆ {0}ᶜ
• spectrum.one_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] : spectrum 𝕜 1 = {1}
• spectrum.zero_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] : spectrum 𝕜 0 = {0}
• AlgHom.apply_mem_spectrum 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {F : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] [FunLike F A R] [AlgHomClass F R A R] [Nontrivial R] (φ : F) (a : A) : φ a ∈ spectrum R a
• AlgHom.spectrum_apply_subset 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) (a : A) : spectrum R (φ a) ⊆ spectrum R a
• spectrum.neg_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) : -spectrum R a = spectrum R (-a)
• AlgEquiv.spectrum_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) : spectrum R (f a) = spectrum R a
• spectrum.scalar_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] (k : 𝕜) : spectrum 𝕜 ((algebraMap 𝕜 A) k) = {k}
• spectrum.setOfPred_isUnit_inter_mul_comm 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a b : A) : {r | IsUnit r} ∩ spectrum R (a * b) = {r | IsUnit r} ∩ spectrum R (b * a)
• spectrum.setOf_isUnit_inter_mul_comm 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a b : A) : {r | IsUnit r} ∩ spectrum R (a * b) = {r | IsUnit r} ∩ spectrum R (b * a)
• spectrum.mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∈ spectrum R a ↔ ¬IsUnit ((algebraMap R A) r - a)
• spectrum.notMem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∉ spectrum R a ↔ IsUnit ((algebraMap R A) r - a)
• spectrum.unit_mem_mul_comm 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a b : A} {r : Rˣ} : ↑r ∈ spectrum R (a * b) ↔ ↑r ∈ spectrum R (b * a)
• spectrum.units_conjugate 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {u : Aˣ} : spectrum R (↑u * a * ↑u⁻¹) = spectrum R a
• spectrum.units_conjugate' 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {u : Aˣ} : spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a
• spectrum.map_inv 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : Aˣ) : (spectrum 𝕜 ↑a)⁻¹ = spectrum 𝕜 ↑a⁻¹
• spectrum.preimage_units_mul_comm 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a b : A) : Units.val ⁻¹' spectrum R (a * b) = Units.val ⁻¹' spectrum R (b * a)
• spectrum.inv₀_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r ∈ spectrum R ↑a⁻¹ → r⁻¹ ∈ spectrum R ↑a
• spectrum.inv₀_mem_inv 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r ∈ spectrum R ↑a → r⁻¹ ∈ spectrum R ↑a⁻¹
• spectrum.of_inv₀_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R ↑a → r ∈ spectrum R ↑a⁻¹
• spectrum.of_inv₀_mem_inv 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R ↑a⁻¹ → r ∈ spectrum R ↑a
• spectrum.inv₀_mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R ↑a ↔ r ∈ spectrum R ↑a⁻¹
• spectrum.inv₀_mem_inv_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} : r⁻¹ ∈ spectrum R ↑a⁻¹ ↔ r ∈ spectrum R ↑a
• spectrum.smul_eq_smul 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] (k : 𝕜) (a : A) (ha : (spectrum 𝕜 a).Nonempty) : spectrum 𝕜 (k • a) = k • spectrum 𝕜 a
• spectrum.add_mem_add_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r s : R} : r + s ∈ spectrum R ((algebraMap R A) s + a) ↔ r ∈ spectrum R a
• spectrum.inv_mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} : ↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹
• spectrum.subset_subalgebra 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [SetLike S A] [SubringClass S A] [SMulMemClass S R A] {s : S} (a : ↥s) : spectrum R ↑a ⊆ spectrum R a
• spectrum.map_star 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [InvolutiveStar R] [StarRing A] [StarModule R A] (a : A) : spectrum R (star a) = star (spectrum R a)
• spectrum.preimage_algebraMap 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} : ⇑(algebraMap R S) ⁻¹' spectrum S a = spectrum R a
• spectrum.unit_smul_eq_smul 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : A) (r : Rˣ) : spectrum R (r • a) = r • spectrum R a
• spectrum.vadd_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : r +ᵥ spectrum R a = spectrum R ((algebraMap R A) r + a)
• spectrum.add_singleton_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : spectrum R a + {r} = spectrum R (a + (algebraMap R A) r)
• spectrum.singleton_add_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : {r} + spectrum R a = spectrum R ((algebraMap R A) r + a)
• spectrum.smul_mem_smul_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {s : R} {r : Rˣ} : r • s ∈ spectrum R (r • a) ↔ s ∈ spectrum R a
• spectrum.add_mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r s : R} : r + s ∈ spectrum R a ↔ r ∈ spectrum R (-(algebraMap R A) s + a)
• spectrum.algebraMap_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} : r ∈ spectrum R a → (algebraMap R S) r ∈ spectrum S a
• spectrum.nonzero_mul_comm 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a b : A) : spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
• spectrum.of_algebraMap_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ spectrum S a → r ∈ spectrum R a
• spectrum.algebraMap_mem_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ spectrum S a ↔ r ∈ spectrum R a
• spectrum.singleton_sub_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : {r} - spectrum R a = spectrum R ((algebraMap R A) r - a)
• spectrum.sub_singleton_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : spectrum R a - {r} = spectrum R (a - (algebraMap R A) r)
• spectrum_subset_quasispectrum 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) : spectrum R a ⊆ quasispectrum R a
• quasispectrum_eq_spectrum_union 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}
• quasispectrum_eq_spectrum_union_zero 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {0}
• mem_quasispectrum_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] {a : A} {x : R} : x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a
• SpectrumRestricts.of_spectrum_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a b : A} {f : S → R} (ha : SpectrumRestricts a f) (h : spectrum S a = spectrum S b) : SpectrumRestricts b f
• spectrum_nonneg_of_nonneg 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {𝕜 : Type u_3} {A : Type u_4} [CommSemiring 𝕜] [PartialOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄ (ha : 0 ≤ a) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) : 0 ≤ x
• SpectrumRestricts.image 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : f '' spectrum S a = spectrum R a
• NonnegSpectrumClass.of_spectrum_nonneg 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {𝕜 : Type u_3} {A : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] : (∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x) → NonnegSpectrumClass 𝕜 A
• SpectrumRestricts.rightInvOn 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
• SpectrumRestricts.subset_preimage 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : spectrum S a ⊆ f ⁻¹' spectrum R a
• NonnegSpectrumClass.iff_spectrum_nonneg 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {𝕜 : Type u_3} {A : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] : NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x
• SpectrumRestricts.apply_mem 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) {s : S} (hs : s ∈ spectrum S a) : f s ∈ spectrum R a
• SpectrumRestricts.algebraMap_image 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : ⇑(algebraMap R S) '' spectrum R a = spectrum S a
• SpectrumRestricts.of_rightInvOn 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (h₁ : Function.LeftInverse f ⇑(algebraMap R S)) (h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)) : SpectrumRestricts a f
• spectrumRestricts_iff 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} : SpectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
• SpectrumRestricts.of_subset_range_algebraMap 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (hf : Function.LeftInverse f ⇑(algebraMap R S)) (h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)) : SpectrumRestricts a f
• Unitization.quasispectrum_eq_spectrum_inr 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : quasispectrum R a = spectrum R ↑a
• Unitization.mem_spectrum_inr_of_not_isUnit 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  {R : Type u_3} {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) (r : R) (hr : ¬IsUnit r) : r ∈ spectrum R ↑a
• Unitization.zero_mem_spectrum_inr 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) (S : Type u_4) {A : Type u_5} [CommSemiring R] [CommRing S] [Nontrivial S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : 0 ∈ spectrum R ↑a
• Unitization.quasispectrum_eq_spectrum_inr' 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_3) (S : Type u_4) {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : quasispectrum R a = spectrum R ↑a
• Pi.spectrum_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Pi
  {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [CommSemiring R] [(i : ι) → Ring (κ i)] [(i : ι) → Algebra R (κ i)] (a : (i : ι) → κ i) : spectrum R a = ⋃ i, spectrum R (a i)
• Prod.spectrum_eq 📋 Mathlib.Algebra.Algebra.Spectrum.Pi
  {A : Type u_2} {B : Type u_3} {R : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (a : A) (b : B) : spectrum R (a, b) = spectrum R a ∪ spectrum R b
• IsStrictlyPositive.spectrum_pos 📋 Mathlib.Algebra.Algebra.StrictPositivity
  {A : Type u_1} {𝕜 : Type u_2} [Ring A] [PartialOrder A] [CommSemiring 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A} (ha : IsStrictlyPositive a) {x : 𝕜} (hx : x ∈ spectrum 𝕜 a) : 0 < x
• Module.End.HasEigenvalue.mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasEigenvalue μ) : μ ∈ spectrum R f
• Module.End.HasUnifEigenvalue.mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasUnifEigenvalue μ 1) : μ ∈ spectrum R f
• Module.End.HasEigenvalue.of_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : μ ∈ spectrum K f → f.HasEigenvalue μ
• Module.End.hasEigenvalue_iff_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasEigenvalue μ ↔ μ ∈ spectrum K f
• Module.End.HasUnifEigenvalue.of_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : μ ∈ spectrum K f → f.HasUnifEigenvalue μ 1
• Module.End.hasUnifEigenvalue_iff_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f
• IsIdempotentElem.finite_spectrum 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  (𝕜 : Type u_1) {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {p : A} (hp : IsIdempotentElem p) : (spectrum 𝕜 p).Finite
• spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  (𝕜 : Type u) {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] [Nontrivial A] [I : FiniteDimensional 𝕜 A] (a : A) : (spectrum 𝕜 a).Nonempty
• IsIdempotentElem.spectrum_subset 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  (𝕜 : Type u_1) {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {p : A} (hp : IsIdempotentElem p) : spectrum 𝕜 p ⊆ {0, 1}
• spectrum.pow_image_subset 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (n : ℕ) : (fun x => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)
• spectrum.pow_mem_pow 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ spectrum 𝕜 a) : k ^ n ∈ spectrum 𝕜 (a ^ n)
• spectrum.map_pow_of_pos 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) : spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
• spectrum.map_pow_of_nonempty 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] {a : A} (ha : (spectrum 𝕜 a).Nonempty) (n : ℕ) : spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
• spectrum.subset_polynomial_aeval 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜) : (fun x => Polynomial.eval x p) '' spectrum 𝕜 a ⊆ spectrum 𝕜 ((Polynomial.aeval a) p)
• spectrum.map_polynomial_aeval_of_nonempty 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hnon : (spectrum 𝕜 a).Nonempty) : spectrum 𝕜 ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum 𝕜 a
• spectrum.map_polynomial_aeval_of_degree_pos 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hdeg : 0 < p.degree) : spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a
• spectrum.exists_mem_of_not_isUnit_aeval_prod 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] {p : Polynomial R} {a : A} (h : ¬IsUnit ((Polynomial.aeval a) (Multiset.map (fun x => Polynomial.X - Polynomial.C x) p.roots).prod)) : ∃ k ∈ spectrum R a, Polynomial.eval k p = 0
• spectrum_diagonal 📋 Mathlib.LinearAlgebra.Eigenspace.Matrix
  {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Field R] (d : n → R) : spectrum R (Matrix.diagonal d) = Set.range d
• Matrix.spectrum_toLin 📋 Mathlib.LinearAlgebra.Eigenspace.Matrix
  {R : Type u_1} {n : Type u_2} {M : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [AddCommGroup M] [Module R M] (A : Matrix n n R) (b : Module.Basis n R M) : spectrum R ((Matrix.toLin b b) A) = spectrum R A
• LinearMap.spectrum_toMatrix 📋 Mathlib.LinearAlgebra.Eigenspace.Matrix
  {R : Type u_1} {n : Type u_2} {M : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (b : Module.Basis n R M) : spectrum R ((LinearMap.toMatrix b b) f) = spectrum R f
• Matrix.spectrum_toLin' 📋 Mathlib.LinearAlgebra.Eigenspace.Matrix
  {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (A : Matrix n n R) : spectrum R (Matrix.toLin' A) = spectrum R A
• LinearMap.spectrum_toMatrix' 📋 Mathlib.LinearAlgebra.Eigenspace.Matrix
  {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (f : (n → R) →ₗ[R] n → R) : spectrum R (LinearMap.toMatrix' f) = spectrum R f
• Matrix.finite_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : (spectrum R A).Finite
• Matrix.instFiniteSpectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : Finite ↑(spectrum R A)
• Module.End.finite_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : (spectrum K f).Finite
• Unitary.spectrum_star_left_conjugate 📋 Mathlib.Algebra.Star.Unitary
  {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} : spectrum R (star ↑U * a * ↑U) = spectrum R a
• Unitary.spectrum_star_right_conjugate 📋 Mathlib.Algebra.Star.Unitary
  {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} : spectrum R (↑U * a * star ↑U) = spectrum R a
• ContinuousLinearMap.spectrum_eq 📋 Mathlib.Analysis.Normed.Operator.Banach
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {f : E →L[𝕜] E} : spectrum 𝕜 f = spectrum 𝕜 ↑f
• Module.End.spectrum_intrinsicStar 📋 Mathlib.Algebra.Star.LinearMap
  {R : Type u_4} {V : Type u_5} [CommRing R] [InvolutiveStar R] [AddCommGroup V] [StarAddMonoid V] [Module R V] [StarModule R V] (f : WithConv (Module.End R V)) : spectrum R (star f).ofConv = star (spectrum R f.ofConv)
• SpectrumRestricts.real_iff 📋 Mathlib.Analysis.Complex.Spectrum
  {A : Type u_1} [Ring A] [Algebra ℂ A] {a : A} : SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re
• Units.continuousOn_inv₀_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [TopologicalSpace R] [ContinuousInv₀ R] [Algebra R A] (a : Aˣ) : ContinuousOn (fun x => x⁻¹) (spectrum R ↑a)
• Units.continuousOn_zpow₀_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [TopologicalSpace R] [ContinuousInv₀ R] [Algebra R A] [ContinuousMul R] (a : Aˣ) (n : ℤ) : ContinuousOn (fun x => x ^ n) (spectrum R ↑a)
• ContinuousFunctionalCalculus.spectrum_nonempty 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst✝ : CommSemiring R} {inst✝¹ : StarRing R} {inst✝² : MetricSpace R} {inst✝³ : IsTopologicalSemiring R} {inst✝⁴ : ContinuousStar R} {inst✝⁵ : Ring A} {inst✝⁶ : StarRing A} {inst✝⁷ : TopologicalSpace A} {inst✝⁸ : Algebra R A} [self : ContinuousFunctionalCalculus R A p] [Nontrivial A] (a : A) (ha : p a) : (spectrum R a).Nonempty
• CFC.spectrum_nonempty 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] (a : A) (ha : p a := by cfc_tac) : (spectrum R a).Nonempty
• ContinuousFunctionalCalculus.isCompact_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) : IsCompact (spectrum R a)
• ContinuousFunctionalCalculus.compactSpace_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst✝ : CommSemiring R} {inst✝¹ : StarRing R} {inst✝² : MetricSpace R} {inst✝³ : IsTopologicalSemiring R} {inst✝⁴ : ContinuousStar R} {inst✝⁵ : Ring A} {inst✝⁶ : StarRing A} {inst✝⁷ : TopologicalSpace A} {inst✝⁸ : Algebra R A} [self : ContinuousFunctionalCalculus R A p] (a : A) : CompactSpace ↑(spectrum R a)
• CFC.spectrum_zero_eq 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] : spectrum R 0 = {0}
• CFC.spectrum_one_eq 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] : spectrum R 1 = {1}
• CFC.eq_zero_of_spectrum_subset_zero 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) : a = 0
• cfc_congr 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A} (hfg : Set.EqOn f g (spectrum R a)) : cfc f a = cfc g a
• CFC.eq_one_of_spectrum_subset_one 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) : a = 1
• CFC.spectrum_algebraMap_eq 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] (r : R) : spectrum R ((algebraMap R A) r) = {r}
• CFC.spectrum_algebraMap_subset 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) : spectrum R ((algebraMap R A) r) ⊆ {r}
• cfc_apply_of_not_continuousOn 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} (a : A) (hf : ¬ContinuousOn f (spectrum R a)) : cfc f a = 0
• cfc_apply_of_not_and 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} (a : A) (ha : ¬(p a ∧ ContinuousOn f (spectrum R a))) : cfc f a = 0
• CFC.eq_algebraMap_of_spectrum_subset_singleton 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (r : R) (h_spec : spectrum R a ⊆ {r}) (ha : p a := by cfc_tac) : a = (algebraMap R A) r
• cfc_map_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : spectrum R (cfc f a) = f '' spectrum R a
• cfc_const_mul 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc (fun x => r * f x) a = r • cfc f a
• cfc_sum_univ 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3} [Fintype ι] (f : ι → R → R) (a : A) (hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac) : cfc (∑ i, f i) a = ∑ i, cfc (f i) a
• cfc_pow 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (n : ℕ) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f x ^ n) a = cfc f a ^ n
• CFC.le_one 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (h : ∀ x ∈ spectrum R a, x ≤ 1) (ha : p a := by cfc_tac) : a ≤ 1
• CFC.one_le 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (h : ∀ x ∈ spectrum R a, 1 ≤ x) (ha : p a := by cfc_tac) : 1 ≤ a
• isUnit_cfc 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : (∀ x ∈ spectrum R a, f x ≠ 0) → IsUnit (cfc f a)
• eqOn_of_cfc_eq_cfc 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A} (h : cfc f a = cfc g a) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : Set.EqOn f g (spectrum R a)
• isUnit_cfc_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0
• cfc_eq_cfc_iff_eqOn 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A} (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) : cfc f a = cfc g a ↔ Set.EqOn f g (spectrum R a)
• cfc_sum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3} (f : ι → R → R) (a : A) (s : Finset ι) (hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac) : cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a
• cfc_nonneg 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} {a : A} (h : ∀ x ∈ spectrum R a, 0 ≤ f x) : 0 ≤ cfc f a
• cfc_nonpos 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ 0) : cfc f a ≤ 0
• algebraMap_le_of_le_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {r : R} {a : A} (h : ∀ x ∈ spectrum R a, r ≤ x) (ha : p a := by cfc_tac) : (algebraMap R A) r ≤ a
• le_algebraMap_of_spectrum_le 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {r : R} {a : A} (h : ∀ x ∈ spectrum R a, x ≤ r) (ha : p a := by cfc_tac) : a ≤ (algebraMap R A) r
• cfc_le_one 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ 1) : cfc f a ≤ 1
• StarOrderedRing.isStrictlyPositive_iff_spectrum_pos 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (a : A) (ha : p a := by cfc_tac) : IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x
• StarOrderedRing.nonneg_iff_spectrum_nonneg 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (a : A) (ha : p a := by cfc_tac) : 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x
• cfcUnits 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : Aˣ
• cfc_comp' 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (g f : R → R) (a : A) (hg : ContinuousOn g (f '' spectrum R a) := by cfc_cont_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => g (f x)) a = cfc g (cfc f a)
• cfc_comp_const_mul 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f ((fun x => r * x) '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (r * x)) a = cfc f (r • a)
• cfc_comp 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (g f : R → R) (a : A) (ha : p a := by cfc_tac) (hg : ContinuousOn g (f '' spectrum R a) := by cfc_cont_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc (g ∘ f) a = cfc g (cfc f a)
• cfc_add_const 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f x + r) a = cfc f a + (algebraMap R A) r
• cfc_const_add 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a
• cfc_add 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (f g : R → R) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) : cfc (fun x => f x + g x) a = cfc f a + cfc g a
• cfc_comp_pow 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (f : R → R) (n : ℕ) (a : A) (hf : ContinuousOn f ((fun x => x ^ n) '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (x ^ n)) a = cfc f (a ^ n)
• cfc_mul 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f g : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) : cfc (fun x => f x * g x) a = cfc f a * cfc g a
• one_le_cfc 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, 1 ≤ f x) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : 1 ≤ cfc f a
• CFC.le_one_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (a : A) (ha : p a := by cfc_tac) : a ≤ 1 ↔ ∀ x ∈ spectrum R a, x ≤ 1
• CFC.one_le_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (a : A) (ha : p a := by cfc_tac) : 1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x
• cfc_map_polynomial 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (q : Polynomial R) (f : R → R) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc (fun x => Polynomial.eval (f x) q) a = (Polynomial.aeval (cfc f a)) q
• val_cfcUnits 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ↑(cfcUnits f a hf' hf ha) = cfc f a
• algebraMap_le_cfc 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (r : R) (a : A) (h : ∀ x ∈ spectrum R a, r ≤ f x) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : (algebraMap R A) r ≤ cfc f a
• cfc_le_algebraMap 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (r : R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ r) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc f a ≤ (algebraMap R A) r
• cfc_isStrictlyPositive_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : IsStrictlyPositive (cfc f a) ↔ ∀ x ∈ spectrum R a, 0 < f x
• cfc_nonneg_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : 0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x
• cfc_mono 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A} (h : ∀ x ∈ spectrum R a, f x ≤ g x) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) : cfc f a ≤ cfc g a
• cfc_comp_star 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (f : R → R) (a : A) (hf : ContinuousOn f (star '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (star x)) a = cfc f (star a)
• cfc_smul 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {S : Type u_3} [SMul S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc (fun x => s • f x) a = s • cfc f a
• cfc_inv 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => (f x)⁻¹) a = Ring.inverse (cfc f a)
• algebraMap_le_iff_le_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] {r : R} {a : A} (ha : p a := by cfc_tac) : (algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x
• le_algebraMap_iff_spectrum_le 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] {r : R} {a : A} (ha : p a := by cfc_tac) : a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r
• cfc_comp_polynomial 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (q : Polynomial R) (f : R → R) (a : A) (hf : ContinuousOn f ((fun x => Polynomial.eval x q) '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (Polynomial.eval x q)) a = cfc f ((Polynomial.aeval a) q)
• val_inv_cfcUnits 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ↑(cfcUnits f a hf' hf ha)⁻¹ = cfc (fun x => (f x)⁻¹) a
• cfc_comp_smul 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] {S : Type u_3} [SMul S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A) (hf : ContinuousOn f ((fun x => s • x) '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (s • x)) a = cfc f (s • a)
• cfcHomSuperset 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : C(↑s, R) →⋆ₐ[R] A
• cfc_comp_inv 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] [ContinuousMap.UniqueHom R A] (f : R → R) (a : Aˣ) (hf : ContinuousOn f ((fun x => x⁻¹) '' spectrum R ↑a) := by cfc_cont_tac) (ha : p ↑a := by cfc_tac) : cfc (fun x => f x⁻¹) ↑a = cfc f ↑a⁻¹
• cfc_comp_neg 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) [ContinuousMap.UniqueHom R A] (hf : ContinuousOn f ((fun x => -x) '' spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f (-x)) a = cfc f (-a)
• cfc_le_one_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc f a ≤ 1 ↔ ∀ x ∈ spectrum R a, f x ≤ 1
• cfc_nonpos_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0
• one_le_cfc_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : 1 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x
• cfc_sub 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f g : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) : cfc (fun x => f x - g x) a = cfc f a - cfc g a
• cfc_map_div 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f g : R → R) (a : A) (hg' : ∀ x ∈ spectrum R a, g x ≠ 0) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc (fun x => f x / g x) a = cfc f a * Ring.inverse (cfc g a)
• algebraMap_le_cfc_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (r : R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : (algebraMap R A) r ≤ cfc f a ↔ ∀ x ∈ spectrum R a, r ≤ f x
• cfcHom 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : C(↑(spectrum R a), R) →⋆ₐ[R] A
• cfc_le_algebraMap_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (r : R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc f a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r
• cfc_comp_zpow 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] [ContinuousMap.UniqueHom R A] (f : R → R) (n : ℤ) (a : Aˣ) (hf : ContinuousOn f ((fun x => x ^ n) '' spectrum R ↑a) := by cfc_cont_tac) (ha : p ↑a := by cfc_tac) : cfc (fun x => f (x ^ n)) ↑a = cfc f ↑(a ^ n)
• cfc_le_iff 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [PartialOrder R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [ContinuousSqrt R] [StarOrderedRing R] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f g : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x
• range_cfc_eq_range_cfcHom 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [StarModule R A] {a : A} (ha : p a) : (Set.range fun x => cfc x a) = ↑(cfcHom ha).range
• cfcL 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : C(↑(spectrum R a), R) →L[R] A
• cfcUnits_pow 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℕ) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfcUnits f a hf' hf ha ^ n = cfcUnits (fun i => f i ^ n) a ⋯ ⋯ ha
• cfcHomSuperset_id 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : (cfcHomSuperset ha hs) (ContinuousMap.restrict s (ContinuousMap.id R)) = a
• cfcHomSuperset_continuous 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : Continuous ⇑(cfcHomSuperset ha hs)
• cfcUnits_zpow 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℤ) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : cfcUnits f a hf' hf ha ^ n = cfcUnits (f ^ n) a ⋯ ⋯ ha
• cfcHom_id 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : (cfcHom ha) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
• cfcHom_injective 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : Function.Injective ⇑(cfcHom ha)
• cfcHom_predicate 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) (f : C(↑(spectrum R a), R)) : p ((cfcHom ha) f)
• cfcHom_continuous 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : Continuous ⇑(cfcHom ha)
• cfcHom_isClosedEmbedding 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ClosedEmbeddingContinuousFunctionalCalculus R A p] {a : A} (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcHom ha)
• ClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst✝ : CommSemiring R} {inst✝¹ : StarRing R} {inst✝² : MetricSpace R} {inst✝³ : IsTopologicalSemiring R} {inst✝⁴ : ContinuousStar R} {inst✝⁵ : Ring A} {inst✝⁶ : StarRing A} {inst✝⁷ : TopologicalSpace A} {inst✝⁸ : Algebra R A} [self : ClosedEmbeddingContinuousFunctionalCalculus R A p] (a : A) (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcHom ha)
• ClosedEmbeddingContinuousFunctionalCalculus.mk 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [toContinuousFunctionalCalculus : ContinuousFunctionalCalculus R A p] (isClosedEmbedding : ∀ (a : A) (ha : p a), Topology.IsClosedEmbedding ⇑(cfcHom ha)) : ClosedEmbeddingContinuousFunctionalCalculus R A p
• cfc_apply 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc f a = (cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }
• cfc_apply_pi 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3} (f : ι → R → R) (a : A) (ha : p a := by cfc_tac) (hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac) : (fun i => cfc (f i) a) = fun i => (cfcHom ha) { toFun := (spectrum R a).domRestrict (f i), continuous_toFun := ⋯ }
• cfc_cases 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0) (haf : ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a), P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })) : P (cfc f a)
• cfcHom_map_spectrum 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) (f : C(↑(spectrum R a), R)) : spectrum R ((cfcHom ha) f) = Set.range ⇑f
• cfcHom_eq_cfc_extend 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (g : R → R) (ha : p a) (f : C(↑(spectrum R a), R)) : (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
• cfc_apply_mkD 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (ha : p a := by cfc_tac) : cfc f a = (cfcHom ha) (ContinuousMap.mkD ((spectrum R a).domRestrict f) 0)
• cfc_def 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_3} {A : Type u_4} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) : cfc f a = if h : p a ∧ ContinuousOn f (spectrum R a) then (cfcHom ⋯) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ } else 0

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59