Commit 2022-04-22 01:34 1da12b57
View on Github →fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544)
This replaces norm_algebra_map_eq : ∀ x : 𝕜, ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥
with norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥
in normed_algebra
. With this change, normed_algebra
means nothing more than "a normed module that is also an algebra", which seems to be the only notion actually used in mathlib anyway. In practice, this change really just removes any constraints on ∥1∥
.
The old meaning of [normed_algebra R A]
is now achieved with [normed_algebra R A] [norm_one_class A]
.
As a result, lemmas like normed_algebra.norm_one_class
and normed_algebra.nontrivial
have been removed, as they no longer make sense now that the two typeclasses are entirely orthogonal.
Notably this means that the following normed_algebra
instances hold more generally than before:
continuous_linear_map.to_normed_algebra
pi.normed_algebra
bounded_continuous_function.normed_algebra
continuous_map.normed_algebra
- Instances not yet in mathlib:
- Matrices under the
L1-L_inf
norm are a normed algebra even if the matrix is empty - Matrices under the frobenius norm are a normed algebra (note
∥(1 : matrix n n 𝕜')∥ = \sqrt (fintype.card n)
with that norm) This last one is the original motivation for this PR; otherwise every lemma about a matrix exponential has to case on whether the matrices are empty. It is possible that some of the[norm_one_class A]
s added inspectrum.lean
are unnecessary; however, the assumptions are no stronger than they were before, and I'm not interested in trying to generalize them as part of this PR. Zulip
- Matrices under the