Submonoid.closure_mul_distrib

Stream: Is there code for X?

[Jireh Loreaux]

Loogle tells me that we don't have the equality version of docs#Submonoid.closure_mul_le under an assumption of commutativity. I assume this means we're missing the corresponding statements for all subobjects in the algebraic hierarchy then. Is that correct?

[Eric Wieser]

I think this is indeed missing

[Eric Wieser]

Probably because it's false?

[Eric Wieser]

Consider addition and S = T = {2}, closure (S + T) = closure {4} < closure {2} = closure S ⊔ closure T.

[Eric Wieser]

Probably it's true if you assume the sets contain an identity element?

[Jireh Loreaux]

Ah yes, I was assuming they contain the Identity.