mathlib3
d36f17f8 - feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)

Commit
4 years ago
feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341) Lemma `is_refl` shows that an alternating sesquilinear form is reflexive. Refactored `sesquilinear_form` in a similar way as `bilinear_form` will be in #10338.
Author
Parents
Loading