Commit 2024-09-10 16:36 608beec8

View on Github →

chore(CategoryTheory/Galois): split out definition from Full file (#16661) Reorganizes the Full file to collect definition and boilerplate code about functorToAction in separate file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Galois/Action.lean

added def CategoryTheory.PreGaloisCategory.functorToAction

added theorem CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq

added theorem CategoryTheory.PreGaloisCategory.functorToAction_map

Modified Mathlib/CategoryTheory/Galois/Full.lean

deleted def CategoryTheory.PreGaloisCategory.functorToAction

deleted theorem CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq