Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 17:39 54c432da

View on Github →

chore(algebra/parity): Reduce imports (#17391) This PR takes the stance that algebra.parity is a basic pure algebra file, and thus moves all the zpow material to algebra.field.basic and algebra.order.field.power, and the irreducible material to algebra.associated.

Estimated changes

added theorem irreducible.not_square
added theorem is_square.not_prime
modified theorem pow_not_prime
added theorem prime.not_square
added theorem bit0_ne_zero
added theorem zero_ne_bit0
added theorem odd.neg_one_zpow
added theorem odd.neg_zpow
modified theorem zpow_bit1_neg
added theorem even.zpow_abs
added theorem even.zpow_pos_iff
added theorem odd.zpow_neg_iff
added theorem odd.zpow_nonpos_iff
added theorem odd.zpow_pos_iff
added theorem zpow_bit0_abs
added theorem zpow_bit0_pos_iff
deleted theorem abs_zpow_bit0
deleted theorem even.abs_zpow
deleted theorem even.zpow_abs
deleted theorem even.zpow_pos
deleted theorem fintype.card_fin_even
deleted theorem irreducible.not_square
deleted theorem is_square.not_irreducible
deleted theorem is_square.not_prime
deleted theorem odd.neg_one_zpow
deleted theorem odd.neg_zpow
deleted theorem odd.zpow_neg
deleted theorem odd.zpow_nonpos
deleted theorem odd.zpow_pos
deleted theorem prime.not_square
deleted theorem zpow_bit0_abs
added theorem fintype.card_fin_even