Commit 2025-05-05 22:46 ef5e381f

View on Github →

feat: add MultilinearMap.ext_ring (#24374) This matches LinearMap.ext_ring. A bunch of downstream proofs now introduce 1 instead of a free variable, hence the removal of arguments to ext.

Estimated changes

Modified Mathlib/Analysis/Analytic/Uniqueness.lean

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

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

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

added theorem AlternatingMap.ext_ring

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

added theorem MultilinearMap.ext_ring

Modified Mathlib/RingTheory/PiTensorProduct.lean

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

added theorem ContinuousAlternatingMap.ext_ring

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

added theorem ContinuousMultilinearMap.ext_ring