Def LinearMap.BilinForm.toMatrixAux

Modification history

2026-01-19 11:57

Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

chore(LinearAlgebra/Matrix/BilinearForm): sort out namespaces (#34057) …

Added LinearMap.BilinForm.toMatrixAux View on Github →