Commit 2022-04-15 02:47 d81cedb1

feat(topology/algebra/module/multilinear): relax requirements for continuous_multilinear_map.mk_pi_algebra (#13426) continuous_multilinear_map.mk_pi_algebra and continuous_multilinear_map.mk_pi_algebra_fin do not need a norm on either the algebra or base ring; all they need is a topology on the algebra compatible with multiplication. The much weaker typeclasses cause some elaboration issues in a few places, as the normed space can no longer be found by unification. Adding a non-dependent version of continuous_multilinear_map.has_op_norm largely resolves this, although a few API proofs about mk_pi_algebra and mk_pi_algebra_fin end up quite underscore heavy. This is the first step in being able to define exp without first choosing a norm.