Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-10 05:27 6152d450

View on Github →

refactor(field_theory/perfect_closure): use bundled homs, review (#2357)

  • refactor(field_theory/perfect_closure): use bundled homs, review Also add lemmas like monoid_hom.iterate_map_mul.
  • Fix a typo spotted by lint
  • Apply suggestions from code review Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

modified def frobenius
modified theorem frobenius_add
modified theorem frobenius_def
modified theorem frobenius_inj
modified theorem frobenius_mul
modified theorem frobenius_nat_cast
modified theorem frobenius_neg
modified theorem frobenius_one
modified theorem frobenius_sub
modified theorem frobenius_zero
added theorem ring_hom.map_frobenius
modified theorem ring_hom.map_pow
added theorem coe_frobenius_equiv
added theorem eq_pth_root_iff
added def frobenius_equiv
modified theorem frobenius_pth_root
deleted theorem is_ring_hom.pth_root
deleted def perfect_closure.UMP
modified theorem perfect_closure.eq_iff'
modified theorem perfect_closure.eq_pth_root
modified theorem perfect_closure.int_cast
modified theorem perfect_closure.mk_zero
modified theorem perfect_closure.nat_cast
added theorem perfect_closure.neg_mk
modified def perfect_closure.of
modified theorem perfect_closure.r.sound
modified inductive perfect_closure.r
modified def perfect_closure
added def pth_root
added theorem pth_root_eq_iff
modified theorem pth_root_frobenius
added theorem ring_hom.map_pth_root