Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-16 09:26 d7f0e686

View on Github →

chore(algebra/group,logic/relator): review some explicit/implicit args (#1441)

  • chore(algebra/group,logic/relator): review some explicit/implicit arguments
  • ring_hom.ext too

Estimated changes

modified theorem monoid_hom.ext
modified theorem divp_eq_iff_mul_eq
modified theorem divp_eq_one_iff_eq
modified theorem units.ext
modified theorem ring_hom.ext