Theorem IsMax.not_infIrred

Modification history

2026-09-07 14:31

Mathlib/Order/Irreducible.lean

chore(Order/Irreducible): use `to_dual` (#43336) …

Deleted IsMax.not_infIrred View on Github →

2023-07-18 11:09

Mathlib/Order/Irreducible.lean

feat: port Order.Irreducible (#5976)

Added IsMax.not_infIrred View on Github →