Theorem CategoryTheory.PreGaloisCategory.not_initial_of_inhabited

Modification history

2024-02-01 20:02
Mathlib/CategoryTheory/Galois/Basic.lean
feat(CategoryTheory/Galois): evaluation is injective and more basic properties (#9841) …
Added CategoryTheory.PreGaloisCategory.not_initial_of_inhabitedView on Github →