Theorems · Theorem · functional analysis
NormedAlgebra.Complex.nonempty_algEquiv
∀ (F : Type u_1) [inst : NormedRing F] [NormOneClass F] [NormMulClass F] [inst_3 : NormedAlgebra ℂ F] [Nontrivial F], Nonempty (ℂ ≃ₐ[ℂ] F)
A version of the Gelfand-Mazur Theorem for nontrivial normed ℂ-algebras F
with multiplicative norm: any such F is isomorphic to ℂ as a ℂ-algebra.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 301 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- Nontrivialstatement and proof · cited by 2,416
- AlgEquivstatement · cited by 1,681
- NormedAlgebrastatement and proof · cited by 1,165
- NormedRingstatement and proof · cited by 924
- NormOneClassstatement and proof · cited by 136
- NormMulClassstatement and proof · cited by 66
- NormedAlgebra.Complex.algEquivOfNormMulproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.