normal_mul — Mathlib

English

For normal N, the carrier of H ⊔ N is the product NH, i.e., the underlying set is NH.

Русский

Для нормального N носитель H ⊔ N равен произведению NH, т.е. подмножество NH.

LaTeX

$$$\\uparrow (H\\lor N) = N H$$$

Lean4

/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when `N` is normal. -/
@[to_additive /-- The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
    when `N` is normal. -/
    ]
theorem normal_mul (N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H :=
  coe_mul_of_right_le_normalizer_left N H le_normalizer_of_normal

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