Theorem Irreducible.map

Modification history

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 →