Commit 2024-10-07 17:59 4c46b674

View on Github →

chore(RamificationInertia): remove superfluous DecidableEq (#17501) Found by the linter in #10235.

Estimated changes

modified theorem Ideal.ramificationIdx_tower