Theorem CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup

Modification history

2024-10-02 09:44
Mathlib/CategoryTheory/Galois/EssSurj.lean
feat(CategoryTheory/Galois): fiber functor is essentially surjective (#16552) …
Added CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroupView on Github →