Theorem Irreducible.map

Modification history

2025-04-17 00:27

Mathlib/Algebra/Prime/Lemmas.lean

feat: additivise `Irreducible` (#22904) …

Deleted Irreducible.map View on Github →

2024-10-25 12:58

Mathlib/Algebra/Associated/Basic.lean

chore(Algebra/Associated): split off Prime and Irreducible (#18224) …

Modified Irreducible.map View on Github →

2024-10-23 11:27

Mathlib/Algebra/Associated/Basic.lean

feat(Algebra/Irreducible): prove irreducibility preserved by `MulEquiv` (#17092) …

Added Irreducible.map View on Github →