Commit 2026-03-23 03:22 1627af05

View on Github →

chore: use abbrev in Archive/Sensitivity (#37011) This avoids some defeq abuse that would require an additional set_option backward.inferInstanceAs.wrap false under v4.29.0-rc7.

Estimated changes

Modified Archive/Sensitivity.lean

modified theorem Sensitivity.Q.card

deleted def Sensitivity.Q