Commit 2023-06-30 13:52 e71da81e

View on Github →

feat: port RingTheory.WittVector.Isocrystal (#5579)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Isocrystal.lean

added def WittVector.FractionRing.frobenius

added def WittVector.FractionRing.frobeniusRingHom

added def WittVector.FractionRing.module

added def WittVector.Isocrystal.frobenius

added structure WittVector.IsocrystalEquiv

added structure WittVector.IsocrystalHom

added theorem WittVector.StandardOneDimIsocrystal.frobenius_apply

added def WittVector.StandardOneDimIsocrystal

added theorem WittVector.isocrystal_classification