Theorem QuadraticMap.IsometryEquiv.coe_symm_toLinearEquiv

Modification history

2026-02-24 20:40
Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean
feat(LinearAlgebra/QuadraticForm): radical of a quadratic form (#34493) …
Added QuadraticMap.IsometryEquiv.coe_symm_toLinearEquivView on Github →