Theorem IsUnit.not_isPrimePow

Modification history

2026-08-03 08:56

Mathlib/Algebra/IsPrimePow.lean

chore: rename `IsPrimePow.not_unit` to `IsPrimePow.not_isUnit` (#42389)

Modified IsUnit.not_isPrimePow View on Github →

2023-01-30 00:50

Mathlib/Algebra/IsPrimePow.lean

feat: Port Algebra.IsPrimePow (#1925)

Added IsUnit.not_isPrimePow View on Github →