Commit 2021-12-30 08:19 655c2f06

chore(topology/algebra/weak_dual_topology): review (#11141)

• Fix universes in pi.has_continuous_smul.
• Add function.injective.embedding_induced and weak_dual.coe_fn_embedding.
• Golf some proofs.
• Review weak_dual.module etc instances to ensure, e.g., module ℝ (weak_dual ℂ E).