Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-10 11:26 0935e8bf

View on Github →

feat(algebra/group/units): add some lemmas about divp (#1388)

  • feat(algebra/group/units): add some lemmas about divp
  • Rename lemmas, add new ones

Estimated changes

added theorem divp_divp_eq_divp_mul
added theorem divp_eq_divp_iff
added theorem divp_eq_iff_mul_eq
deleted theorem divp_eq_one
added theorem divp_eq_one_iff_eq
added theorem divp_inv
added theorem divp_mul_divp