big_sepM2 and associated lemmas
Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.
Would like to hear your comments and also add some helpful lemmas about this big op.
Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.
Would like to hear your comments and also add some helpful lemmas about this big op.