Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bilin_form.nondenerate_dual_prod

Modification history

2023-07-26 13:39

src/linear_algebra/quadratic_form/dual.lean

feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)

Added bilin_form.nondenerate_dual_prod View on Github →