Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 04:59 f44a5eb1

View on Github →

feat(category_theory/concrete_category): id_apply, comp_apply (#7530) This PR renames

  • category_theory.coe_id to category_theory.id_apply
  • category_theory.coe_comp to category_theory.comp_apply The names that are hence free up are then redefined for "unapplied" versions of the same lemmas. The elementwise tactic uses the old lemmas (with their new names). We need minor fixes in the rest of the library because of the name changes.

Estimated changes

modified theorem category_theory.coe_comp
modified theorem category_theory.coe_id