mathlib

d81cedb1 - feat(topology/algebra/module/multilinear): relax requirements for `continuous_multilinear_map.mk_pi_algebra` (#13426)

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`.