Skip to content

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

Jacques-Henri Jourdanrequested to merge
jh/own_big_op into master

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

Merge request reports