Theorem MultilinearMap.alternatization_compLinearMap

Modification history

2026-10-29 21:19
Mathlib/LinearAlgebra/Alternating/Basic.lean
feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …
Modified MultilinearMap.alternatization_compLinearMapView on Github →
2026-09-15 11:27
Mathlib/LinearAlgebra/Alternating/Basic.lean
chore(LinearAlgebra/Alternating/Basic): missing `alternatization_compLinearMap` lemma (#43721)
Added MultilinearMap.alternatization_compLinearMapView on Github →