Theorem QuadraticMap.PosDef.add

Modification history

2024-10-24 21:25
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)
Modified QuadraticMap.PosDef.addView on Github →
2024-08-07 07:08
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
chore: backports for leanprover/lean4#4814 (part 22) (#15511)
Modified QuadraticMap.PosDef.addView on Github →
2024-07-13 17:36
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise `QuadraticForm` to `QuadraticMap` (#7569) …
Added QuadraticMap.PosDef.addView on Github →