non_trivial — Mathlib

English

The pair (F, Aut F) forms a fundamental group object, with naturality, transitivity on Galois fibers, continuity of action, and a nontriviality condition.

Русский

Пара (F, Aut F) образует фундаментальную группу объекта, удовлетворяющую естественности, транситивности на Galois-волокнах, непрерывности действия и некотрой условной не тривиальности.

LaTeX

$$$\text{IsFundamentalGroup}(F,\mathrm{Aut}(F))$$$

Lean4

theorem non_trivial (g : G) (h : ∀ (X : C) (x : F.obj X), g • x = x) : g = 1 :=
  IsFundamentalGroup.non_trivial' g h

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