mathlib

075b3f7d - feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms (#15906)

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`. Co-authored-by: Moritz Doll <doll@uni-bremen.de>