ext — Mathlib

English

Two AutGalois automorphisms are equal if their π projections agree on all pointed Galois objects.

Русский

Два автоморфизма AutGalois равны, если их π-проекции совпадают на всех точечных Galois-объектах.

LaTeX

$$$\forall f,g:\ AutGalois F, (\forall A, AutGalois.\pi F A f = AutGalois.\pi F A g) \Rightarrow f=g$$$

Lean4

/-- Equality of elements of `AutGalois F` can be checked on the projections on each pointed
Galois object. -/
theorem ext {f g : AutGalois F} (h : ∀ (A : PointedGaloisObject F), AutGalois.π F A f = AutGalois.π F A g) : f = g :=
  by
  dsimp only [AutGalois]
  ext A
  exact h A

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