Commit 2025-02-18 20:53 8e3dd4c2

View on Github →

chore(Data/Nat): split Defs into Init and Basic (#22008) This PR follows the instructions in a TODO comment in Data/Nat/Defs.lean to split it into an Init.lean file for everything that doesn't meaningfully depend on Mathlib, and a Basic.lean file for things that do. I redid a few proofs in Nat.Init so they are provable without reference to Mathlib.

Estimated changes

added theorem Nat.dvd_left_injective
added theorem Nat.dvd_sub'
added theorem Nat.leRecOn_injective
added theorem Nat.leRecOn_surjective
added theorem Nat.pow_eq_self_iff
added theorem Nat.pow_left_injective
added theorem Nat.set_induction
added theorem Nat.succ_injective
deleted theorem Nat.dvd_left_injective
deleted theorem Nat.dvd_sub'
deleted theorem Nat.leRecOn_injective
deleted theorem Nat.leRecOn_surjective
deleted theorem Nat.pow_eq_self_iff
deleted theorem Nat.pow_left_injective
deleted theorem Nat.set_induction
deleted theorem Nat.set_induction_bounded
deleted theorem Nat.succ_injective
modified theorem Nat.succ_ne_succ