Commit 2024-07-17 12:28 bf1deba3
View on Github →chore: swap the direction of some ext_iff lemmas (#14796)
In lean 4.11, the @[ext] attribute will generate ext_iff lemmas automatically, following the mathlib convention of putting the 'plain' equality on the left hand side. Some existing lemmas didn't follow this convention; this PR changes that.