Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-09 22:14 aef5c88d

View on Github →

feat(algebra/group_power): more gpow lemmas

Estimated changes

modified theorem add_monoid.neg_smul
added theorem div_pow
added theorem division_ring.inv_pow
modified def gpow
added theorem gpow_bit0
added theorem gpow_bit1
added theorem gpow_coe_nat
added theorem gpow_mul
added theorem gpow_neg
added theorem gpow_neg_one
added theorem gpow_one
added theorem gpow_zero
added theorem gsmul_bit1
added theorem gsmul_mul
added theorem gsmul_neg
added theorem gsmul_neg_one
added theorem gsmul_one
added theorem inv_gpow
modified theorem inv_pow
added theorem one_div_pow
added theorem one_gpow
deleted theorem pow_inv
modified theorem pow_ne_zero