symm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `N`-conjugacy is symmetric. -/
@[to_additive /-- `N`-conjugacy is symmetric. -/
    ]
theorem symm {s₁ s₂ : S.Splitting} (h : S.IsConj s₁ s₂) : S.IsConj s₂ s₁ :=
  by
  obtain ⟨n, hn⟩ := h
  exact ⟨n⁻¹, by simp only [hn, map_inv]; group⟩

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