Mathlib v3 is deprecated. Go to Mathlib v4

Theorem of_irreducible_mul

Modification history

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