Mathlib Map

Theorems · Definition · functional analysis

NormedAlgebra.Complex.algEquivOfNormMul

(F : Type u_1) →
  [inst : NormedRing F] →
    [NormOneClass F] → [NormMulClass F] → [inst_3 : NormedAlgebra ℂ F] → [Nontrivial F] → ℂ ≃ₐ[ℂ] F

A version of the Gelfand-Mazur Theorem. If F is a nontrivial normed ℂ-algebra with multiplicative norm, then we obtain a ℂ-algebra equivalence with ℂ.

Defined in
Mathlib.Analysis.Normed.Algebra.GelfandMazur
Cited by
1 results in Mathlib
Foundations
Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedRingNormOneClassNormMulClassNormedAlgebraNontrivial
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NormedAlgebra.Complex.nonempty_algEquiv · cited by 0Complex.nonempty_algEquivComplex · cited by 5565ComplexNontrivial · cited by 2416NontrivialAlgEquiv · cited by 1681AlgEquivNormedAlgebra · cited by 1165NormedAlgebraNormedRing · cited by 924NormedRingAlgebra.ofId · cited by 166Algebra.ofIdNormOneClass · cited by 136NormOneClassNormMulClass · cited by 66NormMulClassAlgEquiv.ofBijective · cited by 34AlgEquiv.ofBijectiveComplex.algEquivOfNormMulCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.