Theorem LinearMap.toMatrix₂Aux_eq

Modification history

2025-10-21 12:12
Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
refactor: generalize LinearMap.toMatrix₂ and Matrix.toLinearMap₂ to sesquilinear forms (#30108) …
Modified LinearMap.toMatrix₂Aux_eqView on Github →
2024-07-16 18:44
Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices (#9334) …
Modified LinearMap.toMatrix₂Aux_eqView on Github →
2023-05-25 08:46
Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
feat: port LinearAlgebra.Matrix.SesquilinearForm (#4315) …
Added LinearMap.toMatrix₂Aux_eqView on Github →