Theorems · Theorem · functional analysis
quasispectrum.zero_mem
∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [Nontrivial R]
(a : A), 0 ∈ quasispectrum R a- Cited by
- 13 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Modulestatement and proof · cited by 20,661
- CommSemiringstatement and proof · cited by 10,911
- Nontrivialstatement and proof · cited by 2,416
- NonUnitalRingstatement and proof · cited by 422
- quasispectrumstatement · cited by 292
- quasispectrum.not_isUnit_memproof · cited by 2
Cited by14
Results whose statement or proof uses this declaration.
- cfcₙ_congrproof · cited by 25
- cfcₙHomSupersetstatement · cited by 7
- continuousOn_cfcₙproof · cited by 3
- norm_cfcₙ_leproof · cited by 3
- cfcₙHomSuperset_applystatement · cited by 3
- norm_cfcₙ_ltproof · cited by 2
- tendsto_cfcₙ_funproof · cited by 2
- nnnorm_cfcₙ_nnreal_ltproof · cited by 2
- cfcₙHomSuperset_idstatement · cited by 2
- continuous_cfcₙHomSuperset_leftstatement · cited by 1
- quasispectrum.nonemptyproof · cited by 1
- cfcₙHomSuperset_continuousstatement and proof · cited by 1