Commit 2024-12-20 05:45 af8d133b

View on Github →

chore: generalize MulEquiv.prime_iff (#20093) Also put the simpler form on the RHS and simplify the proofs that use it.

Estimated changes

Modified Mathlib/Algebra/Prime/Lemmas.lean

modified theorem MulEquiv.prime_iff

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean