Theorem QuadraticMap.half_moduleEnd_apply_eq_half_smul

Modification history

2024-11-23 08:16
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
feat(LinearAlgebra/QuadraticForm/Basic): weaken invertibility hypothesis on 2 (#14986) …
Added QuadraticMap.half_moduleEnd_apply_eq_half_smulView on Github →