Commit 2023-03-22 14:30 accbdce4

View on Github →

feat: port LinearAlgebra.SesquilinearForm (#2607)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/SesquilinearForm.lean

added theorem LinearMap.IsAdjointPair.add

added theorem LinearMap.IsAdjointPair.comp

added theorem LinearMap.IsAdjointPair.mul

added theorem LinearMap.IsAdjointPair.smul

added theorem LinearMap.IsAdjointPair.sub

added def LinearMap.IsAdjointPair

added theorem LinearMap.IsAlt.isRefl

added theorem LinearMap.IsAlt.neg

added theorem LinearMap.IsAlt.ortho_comm

added theorem LinearMap.IsAlt.self_eq_zero

added def LinearMap.IsAlt

added def LinearMap.IsOrtho

added theorem LinearMap.IsOrthoᵢ.nondegenerateOfNotIsOrthoBasisSelf

added theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft

added theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight

added theorem LinearMap.IsOrthoᵢ.separatingLeftOfNotIsOrthoBasisSelf

added theorem LinearMap.IsOrthoᵢ.separatingRightIffNotIsOrthoBasisSelf

added def LinearMap.IsOrthoᵢ

added def LinearMap.IsPairSelfAdjoint

added theorem LinearMap.IsRefl.domRestrictRefl

added theorem LinearMap.IsRefl.eq_zero

added theorem LinearMap.IsRefl.flip_isRefl_iff

added theorem LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot

added theorem LinearMap.IsRefl.ker_flip_eq_bot

added theorem LinearMap.IsRefl.nondegenerateOfSeparatingLeft

added theorem LinearMap.IsRefl.nondegenerateOfSeparatingRight

added theorem LinearMap.IsRefl.ortho_comm

added def LinearMap.IsRefl

added def LinearMap.IsSkewAdjoint

added theorem LinearMap.IsSymm.domRestrictSymm

added theorem LinearMap.IsSymm.isRefl

added theorem LinearMap.IsSymm.ortho_comm

added def LinearMap.IsSymm

added def LinearMap.Nondegenerate

added theorem LinearMap.SeparatingLeft.congr

added theorem LinearMap.SeparatingLeft.ne_zero

added def LinearMap.SeparatingLeft

added def LinearMap.SeparatingRight

added theorem LinearMap.flip_nondegenerate

added theorem LinearMap.flip_separatingLeft

added theorem LinearMap.flip_separatingRight

added theorem LinearMap.isAdjointPairId

added theorem LinearMap.isAdjointPairZero

added theorem LinearMap.isAdjointPair_iff_comp_eq_compl₂

added theorem LinearMap.isAlt_iff_eq_neg_flip

added theorem LinearMap.isCompl_span_singleton_orthogonal

added theorem LinearMap.isOrthoZeroLeft

added theorem LinearMap.isOrthoZeroRight

added theorem LinearMap.isOrtho_def

added theorem LinearMap.isOrtho_flip

added theorem LinearMap.isOrthoᵢ_def

added theorem LinearMap.isOrthoᵢ_flip

added def LinearMap.isPairSelfAdjointSubmodule

added theorem LinearMap.isPairSelfAdjoint_equiv

added theorem LinearMap.isSkewAdjoint_iff_neg_self_adjoint

added theorem LinearMap.isSymm_iff_eq_flip

added theorem LinearMap.linearIndependent_of_isOrthoᵢ

added theorem LinearMap.mem_isPairSelfAdjointSubmodule

added theorem LinearMap.mem_selfAdjointSubmodule

added theorem LinearMap.mem_skewAdjointSubmodule

added theorem LinearMap.nondegenerateRestrictOfDisjointOrthogonal

added theorem LinearMap.not_separatingLeft_zero

added theorem LinearMap.ortho_smul_left

added theorem LinearMap.ortho_smul_right

added theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker

added def LinearMap.selfAdjointSubmodule

added theorem LinearMap.separatingLeft_congr_iff

added theorem LinearMap.separatingLeft_iff_ker_eq_bot

added theorem LinearMap.separatingLeft_iff_linear_nontrivial

added theorem LinearMap.separatingRight_iff_flip_ker_eq_bot

added theorem LinearMap.separatingRight_iff_linear_flip_nontrivial

added def LinearMap.skewAdjointSubmodule

added theorem LinearMap.span_singleton_inf_orthogonal_eq_bot

added theorem LinearMap.span_singleton_sup_orthogonal_eq_top

added theorem Submodule.le_orthogonalBilin_orthogonalBilin

added theorem Submodule.mem_orthogonalBilin_iff

added def Submodule.orthogonalBilin

added theorem Submodule.orthogonalBilin_le