Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-15 15:46 5806a946

View on Github →

feat(data/nat/basic, data/nat/prime): add various lemmas (#7171)

Estimated changes

Modified src/algebra/ordered_ring.lean

added theorem lt_mul_of_one_lt_left

modified theorem lt_mul_of_one_lt_right

Modified src/data/nat/basic.lean

added theorem nat.dvd_sub'

added theorem nat.pow_two_sub_pow_two

Modified src/data/nat/prime.lean

modified theorem nat.mem_factors

added theorem nat.prime_of_mem_factors

Modified src/data/padics/padic_norm.lean

Modified src/data/pnat/factors.lean

Modified src/number_theory/arithmetic_function.lean

Modified src/ring_theory/int/basic.lean