Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-25 09:58 2b955327

View on Github →

refactor(*): use [fact p.prime] for frobenius and perfect_closure (#2518) This also removes the dependency of algebra.char_p on data.padics.padic_norm, which was only there to make nat.prime a class. I also used this opportunity to rename all alphas and betas to K and L in the perfect closure file.

Estimated changes

modified theorem frobenius_inj
modified theorem coe_frobenius_equiv
modified theorem coe_frobenius_equiv_symm
modified theorem eq_pth_root_iff
modified def frobenius_equiv
modified theorem frobenius_pth_root
modified theorem monoid_hom.map_pth_root
modified theorem perfect_closure.eq_iff'
modified theorem perfect_closure.eq_iff
modified theorem perfect_closure.eq_pth_root
modified theorem perfect_closure.int_cast
modified def perfect_closure.lift
modified theorem perfect_closure.lift_on_mk
modified def perfect_closure.mk
modified theorem perfect_closure.mk_add_mk
modified theorem perfect_closure.mk_mul_mk
modified theorem perfect_closure.mk_zero
modified theorem perfect_closure.nat_cast
modified theorem perfect_closure.neg_mk
modified def perfect_closure.of
modified theorem perfect_closure.of_apply
modified theorem perfect_closure.one_def
modified theorem perfect_closure.r.sound
modified inductive perfect_closure.r
modified theorem perfect_closure.zero_def
modified def perfect_closure
modified def pth_root
modified theorem pth_root_eq_iff
modified theorem pth_root_frobenius
modified theorem ring_hom.map_pth_root