Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 04:10 a31d06a7

View on Github →

feat(data/zmod/basic): Explicitly state computable right_inverses instead of just surjectivity (#5797)

Estimated changes

Modified src/data/zmod/basic.lean

added theorem zmod.int_cast_right_inverse

added theorem zmod.nat_cast_right_inverse

added theorem zmod.ring_hom_right_inverse

modified theorem zmod.ring_hom_surjective