mem_units_iff_val_mem — Mathlib

English

For H ⊆ Units(G) and x ∈ Units(G), x ∈ H.units iff x.val ∈ H

Русский

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

LaTeX

$$$x \\in H^{\\mathrm{units}} \\iff x.{\\text{val}} \\in H$$$

Lean4

@[to_additive]
theorem mem_units_iff_val_mem (H : Subgroup G) (x : Gˣ) : x ∈ H.units ↔ (x : G) ∈ H := by
  simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]

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