Commit 2026-09-15 11:27 59e84018

View on Github →

chore(LinearAlgebra/Alternating/Basic): missing alternatization_compLinearMap lemma (#43721)

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

added theorem MultilinearMap.alternatization_compLinearMap