Commit 2025-09-11 16:39 c9245092

View on Github →

chore: minor golfing in Mathlib.Data.Subtype (#29490)

Estimated changes

modified theorem Subtype.coe_eq_iff