Commit 2025-01-06 14:36 f0c7c5c0

View on Github →

feat(ContinuousMultilinearMap): add lemmas about .prod (#20462)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

added theorem ContinuousMultilinearMap.add_prod_add

added theorem ContinuousMultilinearMap.eq_prod_iff

added theorem ContinuousMultilinearMap.neg_prod_neg

added def ContinuousMultilinearMap.prodEquiv

added theorem ContinuousMultilinearMap.prod_ext

added theorem ContinuousMultilinearMap.prod_ext_iff

added theorem ContinuousMultilinearMap.smul_prod_smul

added theorem ContinuousMultilinearMap.sub_prod_sub

added theorem ContinuousMultilinearMap.zero_prod_zero