mem_ofUnits_iff_toUnits_mem — Mathlib

English

For H ⊆ Units(G) and x ∈ G, x ∈ H.ofUnits iff toUnits x ∈ H.

Русский

Для H ⊆ Units(G) и x ∈ G, x ∈ H.ofUnits тогда и только тогда, когда toUnits(x) ∈ H.

LaTeX

$$$x \\in H^{\\mathrm{ofUnits}} \\iff (\\operatorname{toUnits} x) \\in H$$$

Lean4

@[to_additive]
theorem mem_ofUnits_iff_toUnits_mem (H : Subgroup Gˣ) (x : G) : x ∈ H.ofUnits ↔ (toUnits x) ∈ H := by
  simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]

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