Commit 2023-06-28 17:51 883250cc

View on Github →

feat: port RingTheory.WittVector.DiscreteValuationRing (#5557)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

added theorem WittVector.coe_mkUnit

added theorem WittVector.discreteValuationRing

added theorem WittVector.exists_eq_pow_p_mul'

added theorem WittVector.exists_eq_pow_p_mul

added theorem WittVector.irreducible

added theorem WittVector.isUnit_of_coeff_zero_ne_zero

added def WittVector.mkUnit

added def WittVector.succNthValUnits