Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-23 10:17 c811dd77

View on Github →

feat(data/nat/mul_ind): multiplicative induction principles (#8514)

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.dvd_div_iff

Created src/data/nat/mul_ind.lean

added def nat.rec_on_mul

added def nat.rec_on_pos_prime_coprime

added def nat.rec_on_prime_coprime

added def nat.rec_on_prime_pow

Modified src/data/nat/pow.lean

added theorem nat.one_lt_pow_iff