Commit 2025-06-11 00:20 17747760

View on Github →

feat: if p = a * b is irreducible, then a = 1 or b = 1 (#24913) From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Irreducible/Defs.lean

added theorem Irreducible.eq_one_or_eq_one

modified theorem of_irreducible_mul