zpowers_le — Mathlib

English

For any g ∈ G and subgroup H ≤ G, the cyclic subgroup generated by g is contained in H if and only if g ∈ H: zpowers g ≤ H ↔ g ∈ H.

Русский

Для любого g ∈ G и подпгруппы H, zpowers(g) ≤ H тогда и только если g ∈ H.

LaTeX

$$$\langle g \rangle \le H \iff g \in H$$$

Lean4

@[to_additive (attr := simp)]
theorem zpowers_le {g : G} {H : Subgroup G} : zpowers g ≤ H ↔ g ∈ H := by
  rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

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