Commit 2022-04-25 11:19 ed10ba23

View on Github →

feat(ring_theory/witt_vector/frobenius): add witt_vector.frobenius_equiv (#13666) This promotes the bijection to an equivalence with an explicit inverse

Estimated changes

Modified src/ring_theory/witt_vector/frobenius.lean

added def witt_vector.frobenius_equiv

Modified src/ring_theory/witt_vector/frobenius_fraction_field.lean

Modified src/ring_theory/witt_vector/isocrystal.lean

modified def witt_vector.fraction_ring.frobenius