Theorem CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty

Modification history

2024-02-08 20:07
Mathlib/CategoryTheory/Galois/Basic.lean
feat(CategoryTheory/Galois): characterisation of connected finite `G`-sets (#10228) …
Added CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonemptyView on Github →