Commit 2023-03-21 13:15 a79e4140

View on Github →

feat: port FieldTheory.PerfectClosure (#2879)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/PerfectClosure.lean

added theorem MonoidHom.map_iterate_pthRoot

added theorem MonoidHom.map_pthRoot

added theorem PerfectClosure.R.sound

added inductive PerfectClosure.R

added theorem PerfectClosure.eq_iff'

added theorem PerfectClosure.eq_iff

added theorem PerfectClosure.eq_pthRoot

added theorem PerfectClosure.frobenius_mk

added theorem PerfectClosure.induction_on

added theorem PerfectClosure.int_cast

added def PerfectClosure.lift

added def PerfectClosure.liftOn

added theorem PerfectClosure.liftOn_mk

added def PerfectClosure.mk

added theorem PerfectClosure.mk_add_mk

added theorem PerfectClosure.mk_inv

added theorem PerfectClosure.mk_mul_mk

added theorem PerfectClosure.mk_zero

added theorem PerfectClosure.mk_zero_zero

added theorem PerfectClosure.nat_cast

added theorem PerfectClosure.nat_cast_eq_iff

added theorem PerfectClosure.neg_mk

added def PerfectClosure.of

added theorem PerfectClosure.of_apply

added theorem PerfectClosure.one_def

added theorem PerfectClosure.quot_mk_eq_mk

added theorem PerfectClosure.zero_def

added def PerfectClosure

added theorem RingHom.map_iterate_pthRoot

added theorem RingHom.map_pthRoot

added theorem coe_frobeniusEquiv

added theorem coe_frobeniusEquiv_symm

added theorem commute_frobenius_pthRoot

added theorem eq_pthRoot_iff

added def frobeniusEquiv

added theorem frobenius_pthRoot

added theorem injective_pow_p

added theorem leftInverse_pthRoot_frobenius

added def pthRoot

added theorem pthRoot_eq_iff

added theorem pthRoot_frobenius

added theorem pthRoot_pow_p'

added theorem pthRoot_pow_p

added theorem rightInverse_pthRoot_frobenius