meet-irreducible element

Stream: Is there code for X?

[Andrew Yang]

Do we have results about meet-irreducible elements in a (semi)lattice?
In particular that there is a decomposition $M = p_1 \wedge \dots \wedge p_n$ into irreducibles when $\ge$ is well-founded.

[Yaël Dillies]

I have their definition and some stuff to do with docs#concept.

[Andrew Yang]

Great! Will it get PR'ed into mathlib in the near future?

[Yaël Dillies]

Let me dig that. I should have time today.

[Yaël Dillies]

@Andrew Yang. Here's a very late update: I've just finished proving Birkhoff's representation theorem (as an order isomorphism, not yet as the equivalence of categories), and your decomposition is exists_sup_irred_decomposition on branch#stone_duality.