Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-27 21:47 8838ff35

View on Github →

feat(algebra/field_power): add fpow_one, one_fpow, fpow_mul, mul_fpow (closes #855)

Estimated changes

modified theorem inv_eq_zero
added theorem neg_inv'
added theorem units.mk0_coe
added theorem fpow_mul
added theorem fpow_one
added theorem mul_fpow
added theorem one_fpow