Commit 2025-04-10 20:30 f37d3bd2

View on Github →

chore: drop prime from Irreducible.isUnit_or_isUnit' and use implicit arguments (#23924)

Estimated changes

Modified Mathlib/Algebra/CharP/Algebra.lean

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Prime/Defs.lean

deleted theorem Irreducible.isUnit_or_isUnit

Modified Mathlib/Algebra/Prime/Lemmas.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/FieldTheory/KummerPolynomial.lean

Modified Mathlib/RingTheory/Polynomial/IrreducibleRing.lean

Modified Mathlib/SetTheory/Cardinal/Divisibility.lean