Theorem QuadraticMap.map_smul

Modification history

2025-04-05 12:10

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

refactor: protect "map_add" lemmas (#23451) …

Deleted QuadraticMap.map_smul View on Github →

2024-07-13 17:36

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise `QuadraticForm` to `QuadraticMap` (#7569) …

Added QuadraticMap.map_smul View on Github →