Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-01 16:14 9e78823c

View on Github →

feat(ring_theory/perfection): perfection and tilt (#5032)

depends on: #5132

Estimated changes

Modified docs/references.bib

Created src/ring_theory/perfection.lean

added theorem mod_p.mul_ne_zero_of_pow_p_ne_zero

added theorem mod_p.pre_val_add

added theorem mod_p.pre_val_eq_zero

added theorem mod_p.pre_val_mk

added theorem mod_p.pre_val_mul

added theorem mod_p.pre_val_zero

added theorem mod_p.v_p_lt_pre_val

added theorem mod_p.v_p_lt_val

added def mod_p

added def monoid.perfection

added theorem pre_tilt.coeff_nat_find_add_ne_zero

added theorem pre_tilt.map_eq_zero

added theorem pre_tilt.val_aux_add

added theorem pre_tilt.val_aux_eq

added theorem pre_tilt.val_aux_mul

added theorem pre_tilt.val_aux_one

added theorem pre_tilt.val_aux_zero

added def pre_tilt

added def ring.perfection.coeff

added theorem ring.perfection.coeff_add_ne_zero

added theorem ring.perfection.coeff_frobenius

added theorem ring.perfection.coeff_ne_zero_of_le

added theorem ring.perfection.coeff_pow_p

added theorem ring.perfection.coeff_pth_root

added theorem ring.perfection.ext

added theorem ring.perfection.frobenius_pth_root

added def ring.perfection.pth_root

added theorem ring.perfection.pth_root_frobenius

added def ring.perfection

added def semiring.perfection

added def tilt