Theorem Irreducible.isUnit_of_mul_self_dvd

Modification history

2026-10-07 11:06
Mathlib/Algebra/Prime/Defs.lean
feat(RingTheory): multiplicity at an irreducible element (#40301) …
Added Irreducible.isUnit_of_mul_self_dvdView on Github →