Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.to_add_pow

Modification history

2020-08-06 16:42

src/algebra/group_power.lean

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

Added int.to_add_pow View on Github →