Commit 2022-10-03 21:49 075b3f7d

feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms (#15906) The main goal of this PR is to move linear_algebra/matrix/bilinear_form to the curried bilinear map form. Since this file as quite few dependencies we copy it to a new file linear_algebra/matrix/sesquilinear_form and then move all the dependencies. The structure is taken literally from linear_algebra/matrix/bilinear_form with generalizations and easier proofs where possible. The new lemmas are named exactly as the old ones with the following changes:

• the namespace changed from bilin_form to linear_map
• bilin is changed to linear_map₂. In case there is the necessity for separate bilinear and semi-bilinear lemmas we use linear_map₂ and linear_mapₛₗ₂
• If bilin is not in the name of a lemma, matrix is changed to matrix₂ to avoid nameclashes with lemmas for linear maps M →ₛₗ[ρ₁₂] N Moreover, the following changes were necessary: linear_algebra/bilinear_map:
• Weakened some typeclass assumptions
• Added bilinear version of sum_repr_mul_repr_mul and moved sesquilinear version to sum_repr_mul_repr_mulₛₗ linear_algebra/matrix/bilinear_form:
• Moved basis.equiv_fun_symm_std_basis to linear_algebra/std_basis
• adjoint_pair section: Removed a few definitions (they are now in linear_algebra/matrix/sesquilinear_form) and added a prime to the names of lemmas that have the same name as the version in linear_algebra/matrix/sesquilinear_form linear_algebra/sesquilinear_form:
• Added a few missing lemmas about left-separating bilinear forms (note that separating_left was previously known as nondegenerate) linear_algebra/std_basis:
• Lemma std_basis_apply' for calculating the application of i' : ι to (std_basis R (λ (_x : ι), R) i) algebra/hom/ring/:
• Lemmas for calculating a ring homomorphism applied to ite 0 1 and ite 1 0 The last two additions are needed to get a reasonable proof for matrix.to_linear_map₂'_aux_std_basis.