Commit 2026-08-03 08:56 c0032752

View on Github →

chore: rename Prime.not_unit to Prime.not_isUnit (#42385)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

Modified Mathlib/Algebra/IsPrimePow.lean

Modified Mathlib/Algebra/Prime/Defs.lean

added theorem Prime.not_isUnit

deleted theorem Prime.not_unit

modified theorem not_prime_one

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean

Modified Mathlib/RingTheory/Polynomial/RationalRoot.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

Modified Mathlib/RingTheory/Unramified/LocalStructure.lean

Modified Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean