Theorems · Theorem · functional analysis

QuasispectrumRestricts.left_inv

∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalRing A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  QuasispectrumRestricts a f → Function.LeftInverse f ⇑(algebraMap R S)

f is a left inverse of algebraMap R S.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

13 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

CommSemiringCommSemiringNonUnitalRingModuleModuleAlgebra