Commit 2022-04-22 01:34 1da12b57

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 in spectrum.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