Documentation
Lean source path
Section index:
Section 1: Separable Case
Section 2: Lifting the Isomorphisms