Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-21 16:45 0ed425fa

View on Github →

feat(ring_theory/perfection): define characteristic predicate of perfection (#5386) Name changes:

  • perfect_field --> perfect_ring (generalization)
  • semiring.perfection --> ring.perfection
  • Original ring.perfection deleted.

Estimated changes

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
added theorem injective_pow_p
modified theorem monoid_hom.map_pth_root
modified def perfect_closure.lift
modified def pth_root
modified theorem pth_root_eq_iff
modified theorem pth_root_frobenius
added theorem pth_root_pow_p'
added theorem pth_root_pow_p
modified theorem ring_hom.map_pth_root
added def perfection.coeff
added theorem perfection.coeff_mk
added theorem perfection.coeff_pow_p
added theorem perfection.ext
added def perfection.lift
added theorem perfection_map.id
added theorem perfection_map.mk'
added theorem perfection_map.of
added structure perfection_map
deleted theorem ring.perfection.ext
modified def ring.perfection
deleted def semiring.perfection