Def WittVector.frobeniusFun

Modification history

2023-06-27 14:42

Mathlib/RingTheory/WittVector/Frobenius.lean

feat: port RingTheory.WittVector.Frobenius (#4887)

Added WittVector.frobeniusFun View on Github →