Theorem ContinuousMultilinearMap.add_prod_add

Modification history

2025-01-06 14:36
Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462)
Added ContinuousMultilinearMap.add_prod_addView on Github →