Commit 2024-01-16 07:51 d5ec07c1

View on Github →

refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps (#9312) Some of the concepts in LinearAlgebra/SesquilinearForm can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations. Further generalisations are likely possible, but the scope of this PR is to only consider changes which do not require non-trivial modifications to other parts of Mathlib, or other sections in SesquilinearForm.lean. Further changes can be considered in subsequent PRs if desired.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

modified def LinearMap.IsAlt

modified def LinearMap.IsOrtho

modified theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self

modified theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self

modified theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self

modified def LinearMap.IsOrthoᵢ

modified theorem LinearMap.IsRefl.nondegenerate_of_separatingLeft

modified theorem LinearMap.IsRefl.nondegenerate_of_separatingRight

modified def LinearMap.IsRefl

modified def LinearMap.Nondegenerate

modified theorem LinearMap.SeparatingLeft.ne_zero

modified def LinearMap.SeparatingLeft

modified def LinearMap.SeparatingRight

modified theorem LinearMap.flip_nondegenerate

modified theorem LinearMap.flip_separatingLeft

modified theorem LinearMap.flip_separatingRight

modified theorem LinearMap.isOrtho_def

modified theorem LinearMap.isOrtho_flip

modified theorem LinearMap.isOrtho_zero_left

modified theorem LinearMap.isOrtho_zero_right

modified theorem LinearMap.isOrthoᵢ_def

modified theorem LinearMap.isOrthoᵢ_flip

modified theorem LinearMap.linearIndependent_of_isOrthoᵢ

modified theorem LinearMap.nondegenerateRestrictOfDisjointOrthogonal

modified theorem LinearMap.not_separatingLeft_zero

modified theorem LinearMap.ortho_smul_left

modified theorem LinearMap.ortho_smul_right

modified theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker

modified theorem LinearMap.separatingLeft_iff_ker_eq_bot

modified theorem LinearMap.separatingLeft_iff_linear_nontrivial

modified theorem LinearMap.separatingRight_iff_flip_ker_eq_bot

modified theorem LinearMap.separatingRight_iff_linear_flip_nontrivial

modified theorem LinearMap.span_singleton_inf_orthogonal_eq_bot

modified def Submodule.orthogonalBilin