Commit 2023-06-11 13:19 b29c8d15

View on Github →

feat: port RingTheory.Perfection (#4629)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Created Mathlib/RingTheory/Perfection.lean

added theorem ModP.mul_ne_zero_of_pow_p_ne_zero

added theorem ModP.preVal_add

added theorem ModP.preVal_eq_zero

added theorem ModP.preVal_mk

added theorem ModP.preVal_mul

added theorem ModP.preVal_zero

added theorem ModP.v_p_lt_preVal

added theorem ModP.v_p_lt_val

added def ModP

added def Monoid.perfection

added def Perfection.coeff

added theorem Perfection.coeff_add_ne_zero

added theorem Perfection.coeff_frobenius

added theorem Perfection.coeff_iterate_frobenius'

added theorem Perfection.coeff_iterate_frobenius

added theorem Perfection.coeff_map

added theorem Perfection.coeff_mk

added theorem Perfection.coeff_ne_zero_of_le

added theorem Perfection.coeff_pow_p'

added theorem Perfection.coeff_pow_p

added theorem Perfection.coeff_pthRoot

added theorem Perfection.ext

added theorem Perfection.frobenius_pthRoot

added theorem Perfection.hom_ext

added def Perfection.lift

added def Perfection.map

added def Perfection.pthRoot

added theorem Perfection.pthRoot_frobenius

added theorem PerfectionMap.comp_equiv'

added theorem PerfectionMap.comp_equiv

added theorem PerfectionMap.comp_map

added theorem PerfectionMap.comp_symm_equiv'

added theorem PerfectionMap.comp_symm_equiv

added theorem PerfectionMap.equiv_apply

added theorem PerfectionMap.hom_ext

added theorem PerfectionMap.id

added theorem PerfectionMap.map_eq_map

added theorem PerfectionMap.map_map

added theorem PerfectionMap.mk'

added theorem PerfectionMap.of

added structure PerfectionMap

added theorem PreTilt.coeff_nat_find_add_ne_zero

added theorem PreTilt.map_eq_zero

added theorem PreTilt.valAux_add

added theorem PreTilt.valAux_eq

added theorem PreTilt.valAux_mul

added theorem PreTilt.valAux_one

added theorem PreTilt.valAux_zero

added def PreTilt

added def Ring.Perfection

added def Ring.perfectionSubring

added def Ring.perfectionSubsemiring

added def Tilt