Theorem Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm.{u}

Modification history

2024-02-26 00:38

Counterexamples/QuadraticForm.lean

refactor(LinearAlgebra/QuadraticForm): Replace `BilinForm` with a scalar valued bi `LinearMap` (#10238) …

Added Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm.{u}View on Github →