Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-29 10:32 84f8b395

View on Github →

chore(data/nat/basic): move iterate_inj to injective.iterate (#2561) Also add versions for surjective and bijective

Estimated changes

Modified src/data/nat/basic.lean

added theorem function.bijective.iterate

added theorem function.injective.iterate

added theorem function.surjective.iterate

added theorem nat.iterate_ind

deleted theorem nat.iterate_inj

Modified src/field_theory/perfect_closure.lean