Commit 2021-11-16 12:48 d36f17f8

View on Github →

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.

Estimated changes

Modified src/linear_algebra/sesquilinear_form.lean

deleted def alt_sesq_form.is_alt

deleted theorem alt_sesq_form.neg

deleted theorem alt_sesq_form.self_eq_zero

deleted theorem refl_sesq_form.eq_zero

deleted def refl_sesq_form.is_refl

deleted theorem refl_sesq_form.ortho_sym

added theorem sesq_form.is_alt.is_refl

added theorem sesq_form.is_alt.neg

added theorem sesq_form.is_alt.ortho_comm

added theorem sesq_form.is_alt.self_eq_zero

added def sesq_form.is_alt

added theorem sesq_form.is_refl.eq_zero

added theorem sesq_form.is_refl.ortho_comm

added def sesq_form.is_refl

added theorem sesq_form.is_symm.is_refl

added theorem sesq_form.is_symm.ortho_comm

added def sesq_form.is_symm

deleted theorem sym_sesq_form.is_refl

deleted def sym_sesq_form.is_sym

deleted theorem sym_sesq_form.ortho_sym

deleted theorem sym_sesq_form.sym