Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-20 09:55 bf22ab3f

View on Github →

feat(linear_algebra/bilinear_form): Unique adjoints with respect to a nondegenerate bilinear form (#7071)

Estimated changes

Modified docs/undergrad.yaml

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.comp_left_injective

added theorem bilin_form.comp_symm_comp_of_nondegenerate_apply

added theorem bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate

added theorem bilin_form.is_adjoint_pair_left_adjoint_of_nondegenerate

added theorem bilin_form.is_adjoint_pair_unique_of_nondegenerate

added theorem bilin_form.symm_comp_of_nondegenerate_left_apply