Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 06:38 2ad9b39a

View on Github →

feat(algebra/associated): add irreducible.not_dvd_one (#12686)

Estimated changes

Modified src/algebra/associated.lean

added theorem irreducible.not_dvd_one

Modified src/data/nat/prime.lean

modified theorem nat.prime.not_dvd_one