Finsupp

📁 Source: Mathlib/Data/Sym/Sym2/Finsupp.lean

Statistics

Metric	Count
Definitions sym2Mul	1
Theorems coe_sym2Mul, mem_sym2_support_of_mul_ne_zero, support_sym2Mul_subset, sym2Mul_apply_mk, sym2_support_eq_preimage_support_mul	5
Total	6

Finsupp

Definitions

Name	Category	Theorems
sym2Mul 📖	CompOp	5 math math: QuadraticMap.sum_polar_sub_repr_sq, support_sym2Mul_subset, coe_sym2Mul, QuadraticMap.apply_linearCombination', sym2Mul_apply_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_sym2Mul 📖	mathematical	—	DFunLike.coe Finsupp Sym2 MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero instFunLike sym2Mul Sym2.mul CommSemigroup.toCommMagma CommMonoid.toCommSemigroup CommMonoidWithZero.toCommMonoid Sym2.map	—	—
mem_sym2_support_of_mul_ne_zero 📖	mathematical	—	Sym2 Finset Finset.instMembership Finset.sym2 support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	left_ne_zero_of_mul right_ne_zero_of_mul
support_sym2Mul_subset 📖	mathematical	—	Finset Sym2 Finset.instHasSubset support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero sym2Mul Finset.sym2	—	support_onFinset_subset mem_sym2_support_of_mul_ne_zero
sym2Mul_apply_mk 📖	mathematical	—	DFunLike.coe Finsupp Sym2 MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero instFunLike sym2Mul MulZeroClass.toMul	—	—
sym2_support_eq_preimage_support_mul 📖	mathematical	—	SetLike.coe Finset Sym2 Finset.instSetLike Finset.sym2 support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Set.preimage Sym2.map DFunLike.coe Finsupp instFunLike Function.support Sym2.mul CommSemigroup.toCommMagma CommMonoid.toCommSemigroup CommMonoidWithZero.toCommMonoid	—	Set.ext Finset.coe_sym2

---

← Back to Index