Commit 2023-07-01 12:38 feef3663

View on Github →

feat: defs and lemmas about multilinear maps (#5610) Forward-port leanprover-community/mathlib#19114

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear.lean

deleted def ContinuousMultilinearMap.domDomCongr

added def ContinuousMultilinearMap.domDomCongrₗᵢ

added theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_le

added theorem ContinuousMultilinearMap.norm_domDomCongr

added theorem ContinuousMultilinearMap.norm_ofSubsingleton_le

modified theorem ContinuousMultilinearMap.norm_restrictScalars

added def ContinuousMultilinearMap.restrictScalarsₗᵢ

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

added def ContinuousMultilinearMap.codRestrict

added def ContinuousMultilinearMap.domDomCongrEquiv