ext — Mathlib

English

If two automorphisms σ1, σ2 are both conjugations for φ, then they are equal.

Русский

Если два автоморфизма σ1, σ2 являются конъюгациями для φ, то они равны.

LaTeX

$$If IsConj φ σ1 and IsConj φ σ2, then σ1 = σ2$$

Lean4

theorem ext {σ₁ σ₂ : K ≃ₐ[k] K} (h₁ : IsConj φ σ₁) (h₂ : IsConj φ σ₂) : σ₁ = σ₂ :=
  AlgEquiv.ext fun x ↦ φ.injective ((h₁.eq x).trans (h₂.eq x).symm)

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