Theorem QuadraticMap.associated_left_inverse'

Modification history

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