Commit 2024-08-01 00:14 00f0e137

View on Github →

chore(DirectSum/Algebra): remove superfluous DecidableEq (#15304) Found by the linter in #10235.

Estimated changes