frobenius): add `witt_vector.frobenius_equiv` (#13666)

Commit

3 years ago

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

Author

eric-wieser

Parents

6d3ca07a

mathlib3 ed10ba23 - feat(ring_theory/witt_vector/frobenius): add `witt_vector.frobenius_equiv` (#13666)

mathlib3
ed10ba23 - feat(ring_theory/witt_vector/frobenius): add `witt_vector.frobenius_equiv` (#13666)