trans — Mathlib

English

If s1 is N-conjugate to s2 and s2 is N-conjugate to s3, then s1 is N-conjugate to s3.

Русский

Если s1 конъюгировано к s2, а s2 конъюгировано к s3, то s1 конъюгировано к s3.

LaTeX

$$$S.IsConj s_1 s_2 \\land S.IsConj s_2 s_3 \\Rightarrow S.IsConj s_1 s_3$$$

Lean4

/-- `N`-conjugacy is transitive. -/
@[to_additive /-- `N`-conjugacy is transitive. -/
    ]
theorem trans {s₁ s₂ s₃ : S.Splitting} (h₁ : S.IsConj s₁ s₂) (h₂ : S.IsConj s₂ s₃) : S.IsConj s₁ s₃ :=
  by
  obtain ⟨n₁, hn₁⟩ := h₁
  obtain ⟨n₂, hn₂⟩ := h₂
  exact ⟨n₁ * n₂, by simp only [hn₁, hn₂, map_mul]; group⟩

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