val_mem_ofUnits_iff_mem — 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 : G) \\in H^{\\mathrm{ofUnits}} \\iff x \\in H $$$

Lean4

@[to_additive (attr := simp)]
theorem val_mem_ofUnits_iff_mem (H : Subgroup Gˣ) (x : Gˣ) : (x : G) ∈ H.ofUnits ↔ x ∈ H := by
  simp_rw [mem_ofUnits_iff_toUnits_mem, toUnits_val_apply]

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