Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-20 06:43 71cf2908

View on Github →

feat(algebra/group/commute): add units.left/right_of_mul (#17595)

  • add units.left_of_mul, units.right_of_mul, units.of_pow, units.of_pow_eq_one;
  • add is_prime_pow.not_unit, is_unit.not_is_prime_pow ;
  • golf.

Estimated changes

modified theorem is_unit.pow
modified theorem is_unit_of_pow_eq_one
modified theorem is_unit_pow_iff
modified theorem is_unit_pow_succ_iff
added def units.of_pow
added theorem is_prime_pow.not_unit
modified theorem not_is_prime_pow_one