Commit 2024-12-12 09:27 07b2399c

View on Github →

refactor: make LinearMap.IsAdjointPair accept bare functions as arguments (#19679)

Estimated changes

Modified Mathlib/Algebra/Lie/SkewAdjoint.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

deleted theorem LinearMap.BilinForm.IsAdjointPair.add

deleted theorem LinearMap.BilinForm.IsAdjointPair.comp

deleted theorem LinearMap.BilinForm.IsAdjointPair.eq

deleted theorem LinearMap.BilinForm.IsAdjointPair.mul

deleted theorem LinearMap.BilinForm.IsAdjointPair.smul

deleted theorem LinearMap.BilinForm.IsAdjointPair.sub

deleted def LinearMap.BilinForm.IsAdjointPair

deleted def LinearMap.BilinForm.IsPairSelfAdjoint

deleted def LinearMap.BilinForm.IsSelfAdjoint

deleted def LinearMap.BilinForm.IsSkewAdjoint

deleted theorem LinearMap.BilinForm.isAdjointPair_id

deleted theorem LinearMap.BilinForm.isAdjointPair_iff_compLeft_eq_compRight

deleted theorem LinearMap.BilinForm.isAdjointPair_zero

deleted def LinearMap.BilinForm.isPairSelfAdjointSubmodule

deleted theorem LinearMap.BilinForm.isPairSelfAdjoint_equiv

deleted theorem LinearMap.BilinForm.isSkewAdjoint_iff_neg_self_adjoint

deleted theorem LinearMap.BilinForm.mem_isPairSelfAdjointSubmodule

deleted theorem LinearMap.BilinForm.mem_selfAdjointSubmodule

deleted theorem LinearMap.BilinForm.mem_skewAdjointSubmodule

deleted def LinearMap.BilinForm.selfAdjointSubmodule

deleted def LinearMap.BilinForm.skewAdjointSubmodule

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

deleted theorem isAdjointPair_toBilin'

deleted theorem isAdjointPair_toBilin

deleted def pairSelfAdjointMatricesSubmodule'

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

modified theorem LinearEquiv.isAdjointPair_symm_iff

modified theorem LinearMap.IsAdjointPair.add

modified theorem LinearMap.IsAdjointPair.comp

modified def LinearMap.IsAdjointPair

modified def LinearMap.IsPairSelfAdjoint

modified def LinearMap.IsSkewAdjoint

modified theorem LinearMap.isAdjointPair_id

added theorem LinearMap.isAdjointPair_one

modified theorem LinearMap.isAdjointPair_zero

modified theorem LinearMap.isOrthogonal_of_forall_apply_same

modified theorem LinearMap.isSkewAdjoint_iff_neg_self_adjoint