Commit 2025-12-19 09:26 55fdf804

View on Github →

chore(LinearAlgebra/Multilinear/Basic.lean): remove erws in restr (#32526)

Estimated changes

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/Logic/Equiv/Set.lean

modified theorem dite_comp_equiv_update