Def WittVector.mkUnit

Modification history

2023-06-28 17:51

Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

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

Added WittVector.mkUnit View on Github →