Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-30 12:33 977063f6

View on Github →

chore(group_theory/congruence): a few simp lemmas (#8452)

  • add con.comap_rel;
  • add @[simp] to con.ker_rel;
  • replace con.comp_mk'_apply with con.coe_mk';
  • [unrelated] add commute.semiconj_by.

Estimated changes

added theorem con.coe_mk'
added theorem con.comap_rel
deleted theorem con.comp_mk'_apply