Commit 2025-12-02 23:20 093e8f31
View on Github →chore: remove some redundant @[measurability] attributes (#32239)
This PR removes the @[measurability] attribute from some lemmas when another form of the lemma is already tagged with @[fun_prop].