Commit 2023-06-06 14:40 8f95ac4d

View on Github →

feat: port LinearAlgebra.QuadraticForm.Prod (#4735)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

added theorem QuadraticForm.Equivalent.pi

added theorem QuadraticForm.Equivalent.prod

added def QuadraticForm.Isometry.pi

added def QuadraticForm.Isometry.prod

added theorem QuadraticForm.PosDef.prod

added theorem QuadraticForm.anisotropic_of_pi

added theorem QuadraticForm.anisotropic_of_prod

added theorem QuadraticForm.nonneg_pi_iff

added theorem QuadraticForm.nonneg_prod_iff

added def QuadraticForm.pi

added theorem QuadraticForm.pi_apply

added theorem QuadraticForm.posDef_pi_iff

added theorem QuadraticForm.posDef_prod_iff

added def QuadraticForm.prod