Commit 2023-06-27 19:13 0e596046

View on Github →

feat: port RingTheory.WittVector.Identities (#5527)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Identities.lean

added theorem WittVector.FractionRing.p_nonzero

added theorem WittVector.coeff_p

added theorem WittVector.coeff_p_one

added theorem WittVector.coeff_p_pow

added theorem WittVector.coeff_p_pow_eq_zero

added theorem WittVector.coeff_p_zero

added theorem WittVector.frobenius_verschiebung

added theorem WittVector.iterate_frobenius_coeff

added theorem WittVector.iterate_verschiebung_coeff

added theorem WittVector.iterate_verschiebung_mul

added theorem WittVector.iterate_verschiebung_mul_coeff

added theorem WittVector.iterate_verschiebung_mul_left

added theorem WittVector.mul_charP_coeff_succ

added theorem WittVector.mul_charP_coeff_zero

added theorem WittVector.p_nonzero

added theorem WittVector.verschiebung_frobenius

added theorem WittVector.verschiebung_frobenius_comm

added theorem WittVector.verschiebung_mul_frobenius

added theorem WittVector.verschiebung_zmod