Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-27 23:53 477338d2

View on Github →

refactor(data/subtype): organise in namespaces, use variables, add two simp-lemmas (#760)

Estimated changes

modified theorem subtype.coe_eta
modified theorem subtype.coe_ext
modified theorem subtype.coe_mk
modified theorem subtype.exists
modified theorem subtype.ext
modified theorem subtype.forall
modified theorem subtype.mk_eq_mk
modified theorem subtype.val_injective
added theorem subtype.val_prop'
added theorem subtype.val_prop