Commit 2025-11-05 14:53 82ce0281
View on Github →feat(Analysis/Normed/Algebra/GelfandMazur): new file (#29649) This adds two versions of the Gelfand-Mazur Theorem:
NormedAlgebra.Complex.nonempty_algEquiv (F : Type*) [NormedRing F] [NormOneClass F]
[NormMulClass F] [NormedAlgebra ℂ F] [Nontrivial F] :
Nonempty (ℂ ≃ₐ[ℂ] F)
NormedAlgebra.Real.nonempty_algEquiv_or (F : Type*) [NormedField F] [NormedAlgebra ℝ F] :
Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)
The version for complex algebras differs in its assumptions from the existing version NormedRing.algEquivComplexOfComplete (nontrivial normed algebra with multiplicative norm vs. complete division ring with submultiplicative norm).
A version for real algebras is not yet in Mathlib; it is needed in the context of implementing (absolute) heights; see Heights.
Following a suggestion by @j-loreaux, we also add some API for the Bornology.cobounded filter.