Commit 2024-08-26 10:46 966a3ce1

View on Github →

refactor(Dual): drop a DecidableEq assumption (#16109) Split DualBases.eval into eval_same and eval_of_ne to avoid a DecidableEq assumption.

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Module.DualBases.coe_dualBasis

modified def Module.DualBases.coeffs

modified theorem Module.DualBases.coeffs_apply