Theorems · Definition · functional analysis

SpectrumRestricts

{R : Type u_3} →
  {S : Type u_4} →
    {A : Type u_5} →
      [inst : Semifield R] →
        [inst_1 : Semifield S] → [inst_2 : Ring A] → [Algebra R A] → [Algebra S A] → [Algebra R S] → A → (S → R) → Prop

A (reducible) alias of QuasispectrumRestricts which enforces stronger type class assumptions on the types involved, as it's really intended for the spectrum. The separate definition also allows for dot notation.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

51 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

SemifieldSemifieldRingAlgebraAlgebraAlgebra