Commit 2023-11-29 00:23 b9d519bb

View on Github →

refactor(*/Multilinear): change *.ofSubsingleton (#8694) Change MultilinearMap.ofSubsingleton and other similar definitions so that they are now equivalences between linear maps and 1-multilinear maps.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear.lean

modified theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton

added theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_id

added theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le

deleted theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_le

modified theorem ContinuousMultilinearMap.norm_ofSubsingleton

added theorem ContinuousMultilinearMap.norm_ofSubsingleton_id

added theorem ContinuousMultilinearMap.norm_ofSubsingleton_id_le

deleted theorem ContinuousMultilinearMap.norm_ofSubsingleton_le

added def ContinuousMultilinearMap.ofSubsingletonₗᵢ

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added theorem ContinuousLinearMap.nnnorm_id

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

modified def AlternatingMap.ofSubsingleton

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

modified def MultilinearMap.ofSubsingleton

added def MultilinearMap.ofSubsingletonₗ

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

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

modified def ContinuousAlternatingMap.ofSubsingleton

modified theorem ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap

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

modified def ContinuousMultilinearMap.ofSubsingleton