Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-17 18:15 276ab17f

View on Github →

feat(linear_algebra/bilinear_form): add lemmas (#10353) From FLT-regular.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.nondegenerate.to_matrix'

added theorem bilin_form.nondegenerate.to_matrix

added theorem bilin_form.nondegenerate_iff_det_ne_zero

deleted theorem bilin_form.nondegenerate_of_det_ne_zero'

added theorem bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero

added theorem bilin_form.nondegenerate_to_bilin'_of_det_ne_zero'

added theorem bilin_form.nondegenerate_to_matrix'_iff

added theorem bilin_form.nondegenerate_to_matrix_iff

added theorem matrix.nondegenerate_to_bilin'_iff

added theorem matrix.nondegenerate_to_bilin'_iff_nondegenerate_to_bilin

added theorem matrix.nondegenerate_to_bilin_iff