mem_normalizer_iff' — Mathlib

English

If g ∈ H.normalizer, then for every h ∈ G, h ∈ H ⇔ g^{-1} h g ∈ H.

Русский

Если g принадлежит нормализатору H, тогда для каждого h ∈ G выполняется h ∈ H ⇔ g^{-1} h g ∈ H.

LaTeX

$$$g \\in H.normalizer \\iff \\forall h : G, h \\in H \\iff g^{-1} h g \\in H$$$

Lean4

@[to_additive]
theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by rw [mul_assoc, ← h, inv_mul_cancel_right]⟩

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