Skip to content

add lemmas for 'separable' propositions

Ralf Jung requested to merge ralf/separable into master

I also had to move the 'pure' lemmas down so that we can have "pure is separable" in that section.

This paves the ground for !843 (closed).

Edited by Ralf Jung

Merge request reports