Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-24 21:14 a998db66

View on Github →

refactor(data/nat/prime): redefine nat.prime as irreducible (#11031)

Estimated changes

Modified archive/100-theorems-list/70_perfect_numbers.lean

Modified archive/imo/imo1969_q1.lean

modified def good_nats

modified theorem imo1969_q1

modified theorem polynomial_not_prime

Modified src/algebra/associated.lean

added theorem irreducible.ne_one

Modified src/algebra/char_p/basic.lean

Modified src/data/int/nat_prime.lean

Modified src/data/nat/prime.lean

modified def nat.min_fac_aux

modified theorem nat.not_prime_one

modified theorem nat.not_prime_zero

added theorem nat.prime.eq_one_or_self_of_dvd

modified theorem nat.prime.ne_zero

modified theorem nat.prime.pos

modified theorem nat.prime.two_le

modified def nat.prime

added theorem nat.prime_def_lt''

added theorem nat.two_le_iff

Modified src/data/zmod/basic.lean

Modified src/dynamics/periodic_pts.lean

Modified src/group_theory/order_of_element.lean

Modified src/group_theory/perm/cycle_type.lean

Modified src/group_theory/specific_groups/cyclic.lean

Modified src/number_theory/divisors.lean

Modified src/number_theory/primorial.lean

modified theorem dvd_choose_of_middling_prime

modified def primorial

modified theorem prod_primes_dvd

Modified src/number_theory/sum_four_squares.lean

Modified src/ring_theory/int/basic.lean

modified theorem irreducible_iff_nat_prime

Modified test/fin_cases.lean