Mathlib v3 is deprecated. Go to Mathlib v4

Def quadratic_form.of_polar

Modification history

2022-06-17 15:08

src/linear_algebra/quadratic_form/basic.lean

refactor(linear_algebra/quadratic_form/basic): generalize to semiring (#14303) …

Added quadratic_form.of_polar View on Github →