Theorem WittVector.coe_mkUnit

Modification history

2023-06-28 17:51

Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

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

Added WittVector.coe_mkUnit View on Github →