Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-04 06:51 bf3b52da

View on Github →

chore(algebra/field/basic): reduce imports (#17331)

Estimated changes

Modified src/algebra/field/basic.lean

deleted theorem zpow_bit1_neg

Created src/algebra/field/power.lean

added theorem zpow_bit1_neg

Modified src/algebra/order/field_defs.lean

Modified src/algebra/parity.lean