Commit 2024-11-06 06:21 bcfba1db

View on Github →

refactor(MultilinearMap): rename fields (#18592) Use map_update_* instead of map_*, so that we can move these lemmas to the root namespace once we introduce MultilinearMapClass.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

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

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

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

deleted theorem AlternatingMap.map_add

deleted theorem AlternatingMap.map_neg

deleted theorem AlternatingMap.map_smul

deleted theorem AlternatingMap.map_sub

added theorem AlternatingMap.map_update_add

added theorem AlternatingMap.map_update_neg

added theorem AlternatingMap.map_update_smul

added theorem AlternatingMap.map_update_sub

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

deleted theorem Matrix.det_updateColumn_smul'

added theorem Matrix.det_updateColumn_smul_left

deleted theorem Matrix.det_updateRow_smul'

added theorem Matrix.det_updateRow_smul_left

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

deleted theorem MultilinearMap.map_neg

deleted theorem MultilinearMap.map_sub

added theorem MultilinearMap.map_update_neg

deleted theorem MultilinearMap.map_update_smul

added theorem MultilinearMap.map_update_smul_left

added theorem MultilinearMap.map_update_sub

Modified Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Multilinear/Pi.lean

Modified Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/RingTheory/PiTensorProduct.lean

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

deleted theorem ContinuousAlternatingMap.map_add

deleted theorem ContinuousAlternatingMap.map_smul

deleted theorem ContinuousAlternatingMap.map_sub

added theorem ContinuousAlternatingMap.map_update_add

added theorem ContinuousAlternatingMap.map_update_smul

added theorem ContinuousAlternatingMap.map_update_sub

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

deleted theorem ContinuousMultilinearMap.map_add

deleted theorem ContinuousMultilinearMap.map_smul

deleted theorem ContinuousMultilinearMap.map_sub

added theorem ContinuousMultilinearMap.map_update_add

added theorem ContinuousMultilinearMap.map_update_smul

added theorem ContinuousMultilinearMap.map_update_sub

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

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