Commit 2023-11-17 11:02 7c1536fc

View on Github →

feat: add and use not_irreducible_pow (#8452) Also rename pow_not_prime theorems to match. not_irreducible_pow is extracted from flt-regular.

Estimated changes

Modified Mathlib/Algebra/Associated.lean

added theorem not_irreducible_pow

added theorem not_prime_pow

deleted theorem of_irreducible_pow

deleted theorem pow_not_prime

Modified Mathlib/Data/Nat/Prime.lean

added theorem Nat.Prime.not_prime_pow'

added theorem Nat.Prime.not_prime_pow

deleted theorem Nat.Prime.pow_not_prime'

deleted theorem Nat.Prime.pow_not_prime

Modified Mathlib/FieldTheory/Perfect.lean