Commit 2022-03-03 23:15 544f45bc

View on Github →

refactor(linear_algebra/bilinear_form): split off matrix part (#12435) The bilinear form file is way too large. The part that concerns matrices is not depended on by the general theory, and belongs in its own file.

Estimated changes

Modified src/algebra/lie/skew_adjoint.lean

Modified src/linear_algebra/bilinear_form.lean

deleted theorem basis.equiv_fun_symm_std_basis

deleted theorem bilin_form.mul_to_matrix'

deleted theorem bilin_form.mul_to_matrix'_mul

deleted theorem bilin_form.mul_to_matrix

deleted theorem bilin_form.mul_to_matrix_mul

deleted theorem bilin_form.nondegenerate.to_matrix'

deleted theorem bilin_form.nondegenerate.to_matrix

deleted theorem bilin_form.nondegenerate_iff_det_ne_zero

deleted theorem bilin_form.nondegenerate_of_det_ne_zero

deleted theorem bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero

deleted theorem bilin_form.nondegenerate_to_bilin'_of_det_ne_zero'

deleted theorem bilin_form.nondegenerate_to_matrix'_iff

deleted theorem bilin_form.nondegenerate_to_matrix_iff

deleted def bilin_form.to_matrix'

deleted theorem bilin_form.to_matrix'_apply

deleted theorem bilin_form.to_matrix'_comp

deleted theorem bilin_form.to_matrix'_comp_left

deleted theorem bilin_form.to_matrix'_comp_right

deleted theorem bilin_form.to_matrix'_mul

deleted theorem bilin_form.to_matrix'_symm

deleted theorem bilin_form.to_matrix'_to_bilin'

deleted theorem bilin_form.to_matrix_apply

deleted def bilin_form.to_matrix_aux

deleted theorem bilin_form.to_matrix_aux_std_basis

deleted theorem bilin_form.to_matrix_basis_fun

deleted theorem bilin_form.to_matrix_comp

deleted theorem bilin_form.to_matrix_comp_left

deleted theorem bilin_form.to_matrix_comp_right

deleted theorem bilin_form.to_matrix_mul

deleted theorem bilin_form.to_matrix_mul_basis_to_matrix

deleted theorem bilin_form.to_matrix_symm

deleted theorem bilin_form.to_matrix_to_bilin

deleted theorem bilinear_form.to_matrix_aux_eq

deleted theorem is_adjoint_pair_to_bilin'

deleted theorem is_adjoint_pair_to_bilin

deleted def matrix.is_adjoint_pair

deleted theorem matrix.is_adjoint_pair_equiv

deleted def matrix.is_self_adjoint

deleted def matrix.is_skew_adjoint

deleted theorem matrix.nondegenerate.to_bilin'

deleted theorem matrix.nondegenerate.to_bilin

deleted theorem matrix.nondegenerate_to_bilin'_iff

deleted theorem matrix.nondegenerate_to_bilin'_iff_nondegenerate_to_bilin

deleted theorem matrix.nondegenerate_to_bilin_iff

deleted def matrix.to_bilin'

deleted theorem matrix.to_bilin'_apply'

deleted theorem matrix.to_bilin'_apply

deleted def matrix.to_bilin'_aux

deleted theorem matrix.to_bilin'_aux_eq

deleted theorem matrix.to_bilin'_aux_std_basis

deleted theorem matrix.to_bilin'_comp

deleted theorem matrix.to_bilin'_std_basis

deleted theorem matrix.to_bilin'_symm

deleted theorem matrix.to_bilin'_to_matrix'

deleted theorem matrix.to_bilin_apply

deleted theorem matrix.to_bilin_basis_fun

deleted theorem matrix.to_bilin_comp

deleted theorem matrix.to_bilin_symm

deleted theorem matrix.to_bilin_to_matrix

deleted theorem mem_pair_self_adjoint_matrices_submodule

deleted theorem mem_self_adjoint_matrices_submodule

deleted theorem mem_skew_adjoint_matrices_submodule

deleted def pair_self_adjoint_matrices_submodule

deleted def self_adjoint_matrices_submodule

deleted def skew_adjoint_matrices_submodule

deleted theorem to_bilin'_aux_to_matrix_aux

Created src/linear_algebra/matrix/bilinear_form.lean

added theorem basis.equiv_fun_symm_std_basis

added theorem bilin_form.mul_to_matrix'

added theorem bilin_form.mul_to_matrix'_mul

added theorem bilin_form.mul_to_matrix

added theorem bilin_form.mul_to_matrix_mul

added theorem bilin_form.nondegenerate.to_matrix'

added theorem bilin_form.nondegenerate.to_matrix

added theorem bilin_form.nondegenerate_iff_det_ne_zero

added 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 def bilin_form.to_matrix'

added theorem bilin_form.to_matrix'_apply

added theorem bilin_form.to_matrix'_comp

added theorem bilin_form.to_matrix'_comp_left

added theorem bilin_form.to_matrix'_comp_right

added theorem bilin_form.to_matrix'_mul

added theorem bilin_form.to_matrix'_symm

added theorem bilin_form.to_matrix'_to_bilin'

added theorem bilin_form.to_matrix_apply

added def bilin_form.to_matrix_aux

added theorem bilin_form.to_matrix_aux_std_basis

added theorem bilin_form.to_matrix_basis_fun

added theorem bilin_form.to_matrix_comp

added theorem bilin_form.to_matrix_comp_left

added theorem bilin_form.to_matrix_comp_right

added theorem bilin_form.to_matrix_mul

added theorem bilin_form.to_matrix_mul_basis_to_matrix

added theorem bilin_form.to_matrix_symm

added theorem bilin_form.to_matrix_to_bilin

added theorem bilinear_form.to_matrix_aux_eq

added theorem is_adjoint_pair_to_bilin'

added theorem is_adjoint_pair_to_bilin

added def matrix.is_adjoint_pair

added theorem matrix.is_adjoint_pair_equiv

added def matrix.is_self_adjoint

added def matrix.is_skew_adjoint

added theorem matrix.nondegenerate.to_bilin'

added theorem matrix.nondegenerate.to_bilin

added theorem matrix.nondegenerate_to_bilin'_iff

added theorem matrix.nondegenerate_to_bilin'_iff_nondegenerate_to_bilin

added theorem matrix.nondegenerate_to_bilin_iff

added def matrix.to_bilin'

added theorem matrix.to_bilin'_apply'

added theorem matrix.to_bilin'_apply

added def matrix.to_bilin'_aux

added theorem matrix.to_bilin'_aux_eq

added theorem matrix.to_bilin'_aux_std_basis

added theorem matrix.to_bilin'_comp

added theorem matrix.to_bilin'_std_basis

added theorem matrix.to_bilin'_symm

added theorem matrix.to_bilin'_to_matrix'

added theorem matrix.to_bilin_apply

added theorem matrix.to_bilin_basis_fun

added theorem matrix.to_bilin_comp

added theorem matrix.to_bilin_symm

added theorem matrix.to_bilin_to_matrix

added theorem mem_pair_self_adjoint_matrices_submodule

added theorem mem_self_adjoint_matrices_submodule

added theorem mem_skew_adjoint_matrices_submodule

added def pair_self_adjoint_matrices_submodule

added def self_adjoint_matrices_submodule

added def skew_adjoint_matrices_submodule

added theorem to_bilin'_aux_to_matrix_aux

Modified src/linear_algebra/quadratic_form/basic.lean

Modified src/ring_theory/trace.lean