Product of submonoid in commutative monoid

Stream: Is there code for X?

[Andrew Yang]

Do we have this somewhere?

example (R : Type*) [comm_monoid R] (N : submonoid R) (M : submonoid R) (x : R) :
  x ∈ N ⊔ M ↔ ∃ (y : N) (z : M), x = y * z := sorry

The best I could find is mem_closure_union_iff, but it is in deprecated/submonoid.

[Yaël Dillies]

Isn't it the definition of the sup on submonoids?

[Yaël Dillies]

docs#submonoid

[Yaël Dillies]

Argh no, docs#submonoid.complete_lattice uses docs#complete_lattice_of_Inf to generate the sup and Sup fields.

[Yaël Dillies]

Either prove your theorem by hand or redefine submonoid.complete_lattice so that it holds true by definition. Either should be fine.

[Kevin Buzzard]

The sup on general submonoids is more complicated -- this only works because of the commutativity assumption

[Eric Wieser]

We have docs#submodule.mem_sup

[Eric Wieser]

Do we not have docs#submonoid.mem_sup?