Commit 2023-12-26 10:38 499d5381

View on Github →

feat: define QuadraticForm.IsOrtho as Q (x + y) = Q x + Q y (#9141) This includes some basic API, and the connection with BilinForm.IsOrtho. The motivation for this definition are the results about vectors commuting in a clifford algebra.

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

added theorem CliffordAlgebra.mul_ι_mul_ι_of_isOrtho

deleted theorem CliffordAlgebra.ι_mul_comm

added theorem CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho

added theorem CliffordAlgebra.ι_mul_ι_comm

added theorem CliffordAlgebra.ι_mul_ι_comm_of_isOrtho

added theorem CliffordAlgebra.ι_mul_ι_mul_of_isOrtho

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem BilinForm.toQuadraticForm_isOrtho

added theorem QuadraticForm.IsOrtho.all

added theorem QuadraticForm.IsOrtho.polar_eq_zero

added theorem QuadraticForm.IsOrtho.zero_left

added theorem QuadraticForm.IsOrtho.zero_right

added def QuadraticForm.IsOrtho

added theorem QuadraticForm.associated_isOrtho

added theorem QuadraticForm.isOrtho_comm

added theorem QuadraticForm.isOrtho_def

added theorem QuadraticForm.isOrtho_polarBilin

added theorem QuadraticForm.ne_zero_of_not_isOrtho_self

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

added theorem QuadraticForm.IsOrtho.inl_inr

added theorem QuadraticForm.IsOrtho.inr_inl

added theorem QuadraticForm.IsOrtho.prod

added theorem QuadraticForm.isOrtho_inl_inl_iff

added theorem QuadraticForm.isOrtho_inr_inr_iff