mul_normal — Mathlib

English

If N is normal, then the carrier of H ⊔ N is the product H N as sets.

Русский

Если N нормальна, то носитель H ⊔ N равен множеству произведения H N.

LaTeX

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

Lean4

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

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