Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-03 20:53 39cea43a

View on Github →

docs(data/subtype): add module docstring (#8900)

Estimated changes

modified def subtype.coind
modified theorem subtype.coind_bijective
modified theorem subtype.coind_injective
modified theorem subtype.coind_surjective
modified def subtype.map
modified theorem subtype.map_id
modified theorem subtype.map_injective
modified theorem subtype.map_involutive
modified def subtype.restrict
modified theorem subtype.restrict_apply