Theorem QuadraticForm.associated_tmul

Modification history

2023-08-25 10:49

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

feat(LinearAlgebra/QuadraticForm/TensorProduct): base change of quadratic forms (#6636)

Added QuadraticForm.associated_tmul View on Github →