Theorem not_irreducible_of_not_isUnit_of_dvdNotUnit

Modification history

2026-08-06 01:28
Mathlib/Algebra/Prime/Lemmas.lean
chore: rename some lemmas containing `not_unit` (#42386)
Added not_irreducible_of_not_isUnit_of_dvdNotUnitView on Github →