Theorem MulEquiv.irreducible_iff

Modification history

2024-10-25 12:58

Mathlib/Algebra/Associated/Basic.lean

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

Modified MulEquiv.irreducible_iff View on Github →

2024-10-23 11:27

Mathlib/Algebra/Associated/Basic.lean

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

Added MulEquiv.irreducible_iff View on Github →