Skip to content
GitLab

Lemmas stating that big ops are commuting with op/sep.

Merged Jacques-Henri Jourdan requested to merge jh/own_big_op into master

@gmevel, this is basically the lemmas we discussed this morning.