Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-22 23:07 43159737

View on Github →

feat(quadratic_form/prod): quadratic forms on product and pi types (#10939) In order to provide the pos_def members, some new API was needed.

Estimated changes

Modified src/linear_algebra/clifford_algebra/equivs.lean

modified def clifford_algebra_complex.Q

Modified src/linear_algebra/quadratic_form/basic.lean

added theorem quadratic_form.anisotropic.eq_zero_iff

added theorem quadratic_form.pos_def.anisotropic

added theorem quadratic_form.pos_def.nonneg

added theorem quadratic_form.pos_def_iff_nonneg

added theorem quadratic_form.pos_def_of_nonneg

added def quadratic_form.sq

Created src/linear_algebra/quadratic_form/prod.lean

added theorem quadratic_form.anisotropic_of_pi

added theorem quadratic_form.anisotropic_of_prod

added theorem quadratic_form.equivalent.pi

added theorem quadratic_form.equivalent.prod

added def quadratic_form.isometry.pi

added def quadratic_form.isometry.prod

added theorem quadratic_form.nonneg_pi_iff

added theorem quadratic_form.nonneg_prod_iff

added def quadratic_form.pi

added theorem quadratic_form.pi_apply

added theorem quadratic_form.pos_def.prod

added theorem quadratic_form.pos_def_pi_iff

added theorem quadratic_form.pos_def_prod_iff

added def quadratic_form.prod