Commit 2025-10-08 12:44 595bf89b

View on Github →

refactor(LinearAlgebra): move SesquilinearForm file in a SesquilinearForm folder (#30277) This is motivated by #30274 where I create a new file in the folder for sesquilinear forms over a star ring.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

deleted theorem LinearEquiv.isAdjointPair_symm_iff

deleted theorem LinearMap.BilinForm.apply_apply_same_eq_zero_iff

deleted theorem LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le

deleted theorem LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent

deleted theorem LinearMap.BilinForm.apply_smul_sub_smul_sub_eq

deleted theorem LinearMap.BilinForm.apply_sq_le_of_symm

deleted theorem LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm

deleted theorem LinearMap.BilinForm.nondegenerate_iff'

deleted theorem LinearMap.BilinForm.nondegenerate_iff

deleted theorem LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker

deleted theorem LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq

deleted theorem LinearMap.BilinMap.isSymm_iff_eq_flip

deleted theorem LinearMap.IsAdjointPair.add

deleted theorem LinearMap.IsAdjointPair.comp

deleted theorem LinearMap.IsAdjointPair.mul

deleted theorem LinearMap.IsAdjointPair.smul

deleted theorem LinearMap.IsAdjointPair.sub

deleted def LinearMap.IsAdjointPair

deleted theorem LinearMap.IsAlt.eq_of_add_add_eq_zero

deleted theorem LinearMap.IsAlt.isRefl

deleted theorem LinearMap.IsAlt.neg

deleted theorem LinearMap.IsAlt.ortho_comm

deleted theorem LinearMap.IsAlt.self_eq_zero

deleted def LinearMap.IsAlt

deleted structure LinearMap.IsNonneg

deleted def LinearMap.IsOrtho

deleted def LinearMap.IsOrthogonal

deleted theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self

deleted theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft

deleted theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight

deleted theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self

deleted theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self

deleted def LinearMap.IsOrthoᵢ

deleted def LinearMap.IsPairSelfAdjoint

deleted structure LinearMap.IsPosSemidef

deleted theorem LinearMap.IsRefl.domRestrict

deleted theorem LinearMap.IsRefl.eq_iff

deleted theorem LinearMap.IsRefl.eq_zero

deleted theorem LinearMap.IsRefl.flip_isRefl_iff

deleted theorem LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot

deleted theorem LinearMap.IsRefl.ker_flip_eq_bot

deleted theorem LinearMap.IsRefl.nondegenerate_iff_separatingLeft

deleted theorem LinearMap.IsRefl.nondegenerate_iff_separatingRight

deleted theorem LinearMap.IsRefl.ortho_comm

deleted def LinearMap.IsRefl

deleted def LinearMap.IsSkewAdjoint

deleted theorem LinearMap.IsSymm.domRestrict

deleted theorem LinearMap.IsSymm.isRefl

deleted theorem LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker

deleted theorem LinearMap.IsSymm.ortho_comm

deleted structure LinearMap.IsSymm

deleted def LinearMap.Nondegenerate

deleted theorem LinearMap.SeparatingLeft.congr

deleted theorem LinearMap.SeparatingLeft.ne_zero

deleted def LinearMap.SeparatingLeft

deleted def LinearMap.SeparatingRight

deleted theorem LinearMap.disjoint_ker_of_nondegenerate_restrict

deleted theorem LinearMap.flip_nondegenerate

deleted theorem LinearMap.flip_separatingLeft

deleted theorem LinearMap.flip_separatingRight

deleted theorem LinearMap.isAdjointPair_id

deleted theorem LinearMap.isAdjointPair_iff_comp_eq_compl₂

deleted theorem LinearMap.isAdjointPair_one

deleted theorem LinearMap.isAdjointPair_zero

deleted theorem LinearMap.isAlt_iff_eq_neg_flip

deleted theorem LinearMap.isCompl_span_singleton_orthogonal

deleted theorem LinearMap.isNonneg_def

deleted theorem LinearMap.isNonneg_zero

deleted theorem LinearMap.isOrtho_def

deleted theorem LinearMap.isOrtho_flip

deleted theorem LinearMap.isOrtho_zero_left

deleted theorem LinearMap.isOrtho_zero_right

deleted theorem LinearMap.isOrthogonal_of_forall_apply_same

deleted theorem LinearMap.isOrthoᵢ_def

deleted theorem LinearMap.isOrthoᵢ_flip

deleted def LinearMap.isPairSelfAdjointSubmodule

deleted theorem LinearMap.isPairSelfAdjoint_equiv

deleted theorem LinearMap.isPosSemidef_def

deleted theorem LinearMap.isPosSemidef_zero

deleted theorem LinearMap.isSkewAdjoint_iff_neg_self_adjoint

deleted theorem LinearMap.isSymm_def

deleted theorem LinearMap.isSymm_iff_eq_flip

deleted theorem LinearMap.isSymm_zero

deleted theorem LinearMap.linearIndependent_of_isOrthoᵢ

deleted theorem LinearMap.mem_isPairSelfAdjointSubmodule

deleted theorem LinearMap.mem_selfAdjointSubmodule

deleted theorem LinearMap.mem_skewAdjointSubmodule

deleted theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal

deleted theorem LinearMap.not_separatingLeft_zero

deleted theorem LinearMap.ortho_smul_left

deleted theorem LinearMap.ortho_smul_right

deleted theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker

deleted def LinearMap.selfAdjointSubmodule

deleted theorem LinearMap.separatingLeft_congr_iff

deleted theorem LinearMap.separatingLeft_iff_ker_eq_bot

deleted theorem LinearMap.separatingLeft_iff_linear_nontrivial

deleted theorem LinearMap.separatingRight_iff_flip_ker_eq_bot

deleted theorem LinearMap.separatingRight_iff_linear_flip_nontrivial

deleted def LinearMap.skewAdjointSubmodule

deleted theorem LinearMap.span_singleton_inf_orthogonal_eq_bot

deleted theorem LinearMap.span_singleton_sup_orthogonal_eq_top

deleted theorem Submodule.le_orthogonalBilin_orthogonalBilin

deleted theorem Submodule.mem_orthogonalBilin_iff

deleted def Submodule.orthogonalBilin

deleted theorem Submodule.orthogonalBilin_le

Created Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

added theorem LinearEquiv.isAdjointPair_symm_iff

added theorem LinearMap.BilinForm.apply_apply_same_eq_zero_iff

added theorem LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le

added theorem LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent

added theorem LinearMap.BilinForm.apply_smul_sub_smul_sub_eq

added theorem LinearMap.BilinForm.apply_sq_le_of_symm

added theorem LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm

added theorem LinearMap.BilinForm.nondegenerate_iff'

added theorem LinearMap.BilinForm.nondegenerate_iff

added theorem LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker

added theorem LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq

added theorem LinearMap.BilinMap.isSymm_iff_eq_flip

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.eq_of_add_add_eq_zero

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 structure LinearMap.IsNonneg

added def LinearMap.IsOrtho

added def LinearMap.IsOrthogonal

added theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self

added theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft

added theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight

added theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self

added theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self

added def LinearMap.IsOrthoᵢ

added def LinearMap.IsPairSelfAdjoint

added structure LinearMap.IsPosSemidef

added theorem LinearMap.IsRefl.domRestrict

added theorem LinearMap.IsRefl.eq_iff

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.nondegenerate_iff_separatingLeft

added theorem LinearMap.IsRefl.nondegenerate_iff_separatingRight

added theorem LinearMap.IsRefl.ortho_comm

added def LinearMap.IsRefl

added def LinearMap.IsSkewAdjoint

added theorem LinearMap.IsSymm.domRestrict

added theorem LinearMap.IsSymm.isRefl

added theorem LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker

added theorem LinearMap.IsSymm.ortho_comm

added structure 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.disjoint_ker_of_nondegenerate_restrict

added theorem LinearMap.flip_nondegenerate

added theorem LinearMap.flip_separatingLeft

added theorem LinearMap.flip_separatingRight

added theorem LinearMap.isAdjointPair_id

added theorem LinearMap.isAdjointPair_iff_comp_eq_compl₂

added theorem LinearMap.isAdjointPair_one

added theorem LinearMap.isAdjointPair_zero

added theorem LinearMap.isAlt_iff_eq_neg_flip

added theorem LinearMap.isCompl_span_singleton_orthogonal

added theorem LinearMap.isNonneg_def

added theorem LinearMap.isNonneg_zero

added theorem LinearMap.isOrtho_def

added theorem LinearMap.isOrtho_flip

added theorem LinearMap.isOrtho_zero_left

added theorem LinearMap.isOrtho_zero_right

added theorem LinearMap.isOrthogonal_of_forall_apply_same

added theorem LinearMap.isOrthoᵢ_def

added theorem LinearMap.isOrthoᵢ_flip

added def LinearMap.isPairSelfAdjointSubmodule

added theorem LinearMap.isPairSelfAdjoint_equiv

added theorem LinearMap.isPosSemidef_def

added theorem LinearMap.isPosSemidef_zero

added theorem LinearMap.isSkewAdjoint_iff_neg_self_adjoint

added theorem LinearMap.isSymm_def

added theorem LinearMap.isSymm_iff_eq_flip

added theorem LinearMap.isSymm_zero

added theorem LinearMap.linearIndependent_of_isOrthoᵢ

added theorem LinearMap.mem_isPairSelfAdjointSubmodule

added theorem LinearMap.mem_selfAdjointSubmodule

added theorem LinearMap.mem_skewAdjointSubmodule

added theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal

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

Modified Mathlib/RingTheory/Polynomial/Wronskian.lean