Theorem Finsupp.mem_sym2_support_of_mul_ne_zero

Modification history

2025-04-06 22:22
Mathlib/Data/Sym/Sym2/Finsupp.lean
feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map (#18578) …
Added Finsupp.mem_sym2_support_of_mul_ne_zeroView on Github →