Commit 2021-08-17 15:24 323e4280

View on Github →

Expand ↑-notation. (#37)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Subtype.lean

deleted theorem Subtype.coe_prop

deleted theorem Subtype.val_eq_coe

modified theorem Subtype.val_prop

Created Mathlib/Tactic/Coe.lean