Theorem Irreducible.of_map

Modification history

2024-10-25 12:58

Mathlib/Algebra/Associated/Basic.lean

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

Modified Irreducible.of_map View on Github →

2024-10-08 12:10

Mathlib/Algebra/Associated/Basic.lean

refactor: generalise `IsLocalRingHom` to monoids (#6045) …

Added Irreducible.of_map View on Github →