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

Commit

5 years ago

feat(algebra/group_power): lemmas relating pow in `multiplicative int` with multiplication in `int` (#3706) Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Author

ChrisHughes24

Parents

35ecc7ba

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

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