Commit 2024-06-01 08:03 5f37a7ea

View on Github →

refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents (#10432) Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap.IsRefl and LinearMap.IsSymm.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

modified theorem LinearMap.BilinForm.IsAlt.isRefl

modified theorem LinearMap.BilinForm.IsAlt.neg_eq

modified theorem LinearMap.BilinForm.IsAlt.self_eq_zero

modified def LinearMap.BilinForm.IsAlt

modified def LinearMap.BilinForm.IsRefl

modified def LinearMap.BilinForm.IsSymm