Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-04 20:49 9a8f1b06

View on Github →

feat(algebra/group_power): gpow_add_one (#683)

feat(algebra/group_power): gpow_add_one
feat(data/nat//basic): int.coe_nat_abs

Estimated changes

Modified src/algebra/group_power.lean

added theorem add_one_gsmul

added theorem gpow_add_one

added theorem gpow_one_add

added theorem one_add_gsmul

Modified src/data/int/basic.lean

added theorem int.coe_nat_abs