Def QuadraticForm.tensorRId

Modification history

2024-07-09 09:09

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean

chore: add missing spaces around = or := (#14554) …

Modified QuadraticForm.tensorRId View on Github →

2023-09-18 15:32

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean

feat(LinearAlgebra/QuadraticForm/TensorProduct): commutativity and associativity (#7223) …

Added QuadraticForm.tensorRId View on Github →