Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-11 10:11 c946d609

View on Github →

chore(data/nat/prime): add 2 aliases (#17372) Add nat.prime.prime and prime.nat_prime. Also move 2 lemmas and golf some proofs.

Estimated changes

Modified src/algebra/associated.lean

added theorem eq_of_prime_pow_eq'

added theorem eq_of_prime_pow_eq

Modified src/algebra/char_p/local_ring.lean

Modified src/algebra/is_prime_pow.lean

deleted theorem eq_of_prime_pow_eq'

deleted theorem eq_of_prime_pow_eq

modified theorem nat.prime.is_prime_pow

Modified src/data/nat/factorization/prime_pow.lean

Modified src/data/nat/prime.lean

modified theorem nat.irreducible_iff_prime

Modified src/field_theory/cardinality.lean

Modified src/group_theory/p_group.lean

Modified src/group_theory/torsion.lean

Modified src/number_theory/von_mangoldt.lean

Modified src/ring_theory/int/basic.lean

Modified src/ring_theory/roots_of_unity.lean