Theorem Finsupp.sym2Mul_apply_mk

Modification history

2026-02-16 15:42
Mathlib/Data/Sym/Sym2/Finsupp.lean
refactor(Data/Sym/Sym2): curry `mk` (#34803) …
Modified Finsupp.sym2Mul_apply_mkView on Github →
2025-04-06 22:22
Mathlib/Data/Sym/Sym2/Finsupp.lean
feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map (#18578) …
Added Finsupp.sym2Mul_apply_mkView on Github →