Mathlib v3 is deprecated. Go to Mathlib v4

Def irreducible

Modification history

2021-02-05 12:11

src/algebra/associated.lean

refactor(*): remove uses of @[class] def (#6028) …

Deleted irreducible View on Github →

2018-09-03 16:58

ring_theory/associated.lean

refactor(ring_theory/associated): rename associated_elements

Modified irreducible View on Github →

2018-09-02 20:50

ring_theory/associated_elements.lean

feat(ring_theory): add associated elements

Added irreducible View on Github →