Commit 2023-10-19 13:16 cf3ecdf9

View on Github →

feat(LinearAlgebra/QuadraticForm/Prod): lemmas about polar,polarBilin, and associated (#7664) This also slightly adjusts the file sectioning in order to introduce the temporary Ring assumption.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm.lean

added theorem BilinForm.sum_apply

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

added theorem QuadraticForm.Ring.associated_pi

added theorem QuadraticForm.Ring.polarBilin_pi

added theorem QuadraticForm.Ring.polar_pi

added theorem QuadraticForm.associated_prod

added theorem QuadraticForm.polarBilin_prod

added theorem QuadraticForm.polar_prod