Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.of_add_mul

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.of_add_mul View on Github →