Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irreducible_or_factor

Modification history

2018-09-03 16:58
ring_theory/associated.lean
refactor(ring_theory/associated): rename associated_elements
Added irreducible_or_factorView on Github →