mem_comm — Mathlib

English

If H ≤ K and (H.subgroupOf K).Normal, then whenever a ∈ H and b ∈ K with ab ∈ H, we have ba ∈ H.

Русский

Если H ≤ K и H подгруппа нормальна в K, то из ab ∈ H следует ba ∈ H для a ∈ H, b ∈ K.

LaTeX

$$$(b a) \in H \text{ whenever } a \in H, b \in K, ab \in H$, given $H \le K$ and $(H \subgroupOf K).Normal$.$$

Lean4

@[to_additive]
theorem mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal] {a b : G} (hb : b ∈ K) (h : a * b ∈ H) :
    b * a ∈ H := by
  have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
  rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this

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