set_mul_normal_comm — Mathlib

English

If N is normal, then the carrier of H ⊔ N is the product set H N: (↑(H ⊔ N)) = H N as sets.

Русский

Если N нормальна, то носитель объединения H ⊔ N равен произведению множеств: (↑(H ⊔ N)) = H N.

LaTeX

$$$(H\\lor N)^{\\uparrow} = H N$$$

Lean4

@[to_additive]
theorem set_mul_normal_comm (S : Set G) (N : Subgroup G) [hN : N.Normal] : S * (N : Set G) = (N : Set G) * S :=
  set_mul_normalizer_comm S N subset_normalizer_of_normal

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