toAutMulEquiv_apply

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply

English

The component of the toAutMulEquiv at g coincides with the component of toAut at g.

Русский

Компонент toAutMulEquiv в g совпадает с компонентом toAut в g.

LaTeX

$$$toAutMulEquiv\,F\,G\ g = toAut\,F\,G\ g$$$

Lean4

@[simp]
theorem toAutMulEquiv_apply (g : G) : toAutMulEquiv F G g = toAut F G g :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru