Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 16:27 14dcfe0c

View on Github →

chore(*): assorted lemmas (#4566) Non-bc changes:

  • make some lemmas use coe instead of subtype.val;
  • make the arguments of range_comp explicit, reorder them.

Estimated changes

modified theorem finsupp.emb_domain_apply
modified theorem finsupp.emb_domain_inj
modified theorem finsupp.emb_domain_zero
modified theorem finsupp.support_emb_domain
added theorem finsupp.unique_ext
added theorem finsupp.unique_ext_iff
added theorem option.cases_on'_coe
added theorem option.cases_on'_none
added theorem option.cases_on'_some
added theorem set.pair_comm
modified theorem set.range_comp
added theorem set.subset_Inter_iff
added theorem sum.injective_inl
added theorem sum.injective_inr
added theorem not_subsingleton