feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map

[mans0954]

Three lemmas about Quadratic maps applied to:

• A finite sum
• A linearCombination
• The representation of an element wrt a basis

---

[github-actions]

PR summary b6cdfd3a4c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Sym.Sym2	480	484	+4 (+0.83%)
Mathlib.LinearAlgebra.QuadraticForm.Basis	1431	1432	+1 (+0.07%)

Import changes for all files

Files	Import difference
21 files Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Surreal.Basic	1
6 files Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Sum	3
29 files Mathlib.Algebra.BigOperators.Sym Mathlib.Combinatorics.Digraph.Orientation Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.LineGraph Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Path Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Data.Finset.Sym Mathlib.Data.List.Sym Mathlib.Data.Multiset.Sym Mathlib.Data.Sym.Card Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Order.GameAdd Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.PGame Mathlib.SetTheory.ZFC.Ordinal	4

---

Declarations diff

+ Sym2.mul_finsupp
+ Sym2.mul_finsupp_support
+ Sym2.testB
+ apply_linearCombination
+ apply_linearCombination'
+ coe_pointwise_module_smul
+ map_finsuppSum
+ map_finsuppSum'
+ mul
+ mul_sym2Mk
+ pointwiseModuleScalar
+ polarSym2_map_mul
+ smul
+ sum_polar_sub_repr_sq
+ sum_repr_sq_add_sum_repr_mul_polar
+ test

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mans0954]

CC: @eric-wieser

[eric-wieser]

I think inheriting a * from a smul in this way is not an established pattern in mathlib. This would maybe be a little less objectionable if it used HSMul, but fundamentally the heterogenous classes create nasty diamond issues (which I touch on briefly in Section 4.8 of my thesis.