Theorems · Inductive type · functional analysis

NormedAlgebra

(𝕜 : Type u_6) → (𝕜' : Type u_7) → [NormedField 𝕜] → [SeminormedRing 𝕜'] → Type (max u_6 u_7)

A normed algebra 𝕜' over 𝕜 is normed module that is also an algebra. See the implementation notes for Algebra for a discussion about non-unital algebras. Following the strategy there, a non-unital normed algebra can be written as: ``lean variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜'] variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] ``

Defined in

Mathlib.Analysis.Normed.Module.Basic

Cited by

1,165 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

NormedFieldSeminormedRing