mem_iff_toUnits_mem_units — Mathlib

English

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

Русский

Пусть H ⊆ Units(G) и x ∈ Units(G). Тогда (x : G) ∈ H.ofUnits тогда и только тогда, когда x ∈ H.

LaTeX

$$$x \\in H^{\\mathrm{ofUnits}} \\iff x \\in H$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_iff_toUnits_mem_units (H : Subgroup G) (x : G) : toUnits x ∈ H.units ↔ x ∈ H := by
  simp_rw [mem_units_iff_val_mem, val_toUnits_apply]

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