Commit 2023-08-14 20:58 75bcb185

View on Github →

chore: refactor perfect rings / fields (#6182) The main changes are:

  • we replace the data-bearing PerfectRing typeclass with a Prop-valued (non-constructive) version,
  • we introduce a new typeclass PerfectField,
  • we add a proof that a perfect field of positive characteristic has surjective Frobenius map,
  • we add some basic facts such as perfection of finite rings / fields and products of perfect rings.

Estimated changes

deleted theorem MonoidHom.iterate_map_mul
deleted theorem RingHom.iterate_map_add
deleted theorem RingHom.iterate_map_mul
added theorem iterate_map_mul
added theorem bijective_frobenius
added theorem coe_frobeniusEquiv
added theorem injective_frobenius
added theorem injective_pow_p
added theorem not_irreducible_expand
added theorem polynomial_expand_eq
added theorem surjective_frobenius
deleted theorem MonoidHom.map_pthRoot
modified theorem PerfectClosure.eq_iff
deleted theorem PerfectClosure.eq_pthRoot
deleted def PerfectClosure.lift
deleted theorem RingHom.map_pthRoot
deleted theorem coe_frobeniusEquiv
deleted theorem coe_frobeniusEquiv_symm
deleted theorem commute_frobenius_pthRoot
deleted theorem eq_pthRoot_iff
deleted def frobeniusEquiv
deleted theorem frobenius_pthRoot
deleted theorem injective_pow_p
deleted def pthRoot
deleted theorem pthRoot_eq_iff
deleted theorem pthRoot_frobenius
deleted theorem pthRoot_pow_p'
deleted theorem pthRoot_pow_p
deleted def Perfection.lift