Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-06 16:42 1930601c

View on Github →

feat(algebra/group_power): lemmas relating pow in multiplicative int with multiplication in int (#3706)

Estimated changes

added theorem int.of_add_mul
added theorem int.to_add_gpow
added theorem int.to_add_pow
added theorem nat.of_add_mul
added theorem nat.to_add_pow