Commit 2021-11-16 21:57 8f7971ae

View on Github →

refactor(linear_algebra/bilinear_form): Change namespace of is_refl, is_symm, and is_alt (#10338) The propositions is_refl, is_symm, and is_alt are now in the namespace bilin_form. Moreover, is_sym is now renamed to is_symm.

Estimated changes

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified src/linear_algebra/bilinear_form.lean

deleted def alt_bilin_form.is_alt

deleted theorem alt_bilin_form.is_refl

deleted theorem alt_bilin_form.neg

deleted theorem alt_bilin_form.ortho_sym

deleted theorem alt_bilin_form.self_eq_zero

added theorem bilin_form.is_alt.is_refl

added theorem bilin_form.is_alt.neg

added theorem bilin_form.is_alt.ortho_comm

added theorem bilin_form.is_alt.self_eq_zero

added def bilin_form.is_alt

added theorem bilin_form.is_refl.eq_zero

added theorem bilin_form.is_refl.ortho_comm

added def bilin_form.is_refl

added theorem bilin_form.is_symm.is_refl

added theorem bilin_form.is_symm.ortho_comm

added def bilin_form.is_symm

added theorem bilin_form.is_symm_iff_flip'

modified theorem bilin_form.le_orthogonal_orthogonal

deleted theorem bilin_form.restrict_sym

added theorem bilin_form.restrict_symm

deleted theorem refl_bilin_form.eq_zero

deleted def refl_bilin_form.is_refl

deleted theorem refl_bilin_form.ortho_sym

deleted theorem sym_bilin_form.is_refl

deleted def sym_bilin_form.is_sym

deleted theorem sym_bilin_form.is_sym_iff_flip'

deleted theorem sym_bilin_form.ortho_sym

deleted theorem sym_bilin_form.sym

Modified src/linear_algebra/quadratic_form/basic.lean

deleted theorem quadratic_form.associated_is_sym

added theorem quadratic_form.associated_is_symm

modified theorem quadratic_form.associated_left_inverse

Modified src/ring_theory/trace.lean

deleted theorem algebra.trace_form_is_sym

added theorem algebra.trace_form_is_symm