Theorem CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app

Modification history

2026-04-14 15:27

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) …

Modified CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app View on Github →

2024-05-14 10:23

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

feat(CategoryTheory/Galois): prorepresentability of fiber functors (#12839) …

Added CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app View on Github →