Commit 2025-03-12 19:14 5342b24b

View on Github →

fix(Group/Pointwise): fix some lemmas (#22729) They used non-heterogeneous symbols like SMul.smul, thus failed to apply to HSMul.hSMul etc.

Estimated changes

modified theorem Set.image2_div
modified theorem Set.image2_smul
modified theorem Set.image2_vsub