Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irreducible_of_prime

Modification history

2021-08-17 18:30
src/algebra/associated.lean
chore(algebra/associated): use more dot notation (#8556) …
Deleted irreducible_of_primeView on Github →
2020-10-26 23:04
src/algebra/associated.lean
chore(*): reflow some long lines (#4794)
Modified irreducible_of_primeView on Github →
2020-08-13 12:59
src/algebra/associated.lean
refactor(algebra/associated): change several instances from [integral_domain] to [comm_cancel_monoid_with_zero] (#3744) …
Modified irreducible_of_primeView on Github →
2018-12-17 09:19
ring_theory/associated.lean
feat(data/polynomial): lemmas relating unit and irreducible with degree (#514)
Added irreducible_of_primeView on Github →