Theorems · Theorem · functional analysis

Unitization.zero_mem_spectrum_inr

∀ (R : Type u_3) (S : Type u_4) {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommRing S] [Nontrivial S]
  [inst_3 : NonUnitalRing A] [inst_4 : Algebra R S] [inst_5 : Module S A] [inst_6 : IsScalarTower S A A]
  [inst_7 : SMulCommClass S A A] [inst_8 : Module R A] [inst_9 : IsScalarTower R S A] (a : A), 0 ∈ spectrum R ↑a

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingNontrivialNonUnitalRingAlgebraModuleIsScalarTowerSMulCommClassModuleIsScalarTower