inv — Mathlib

English

If H is a subgroup of a group G, then H is itself a group under the same operation, and the inverse of any element h in H (taken in G) lies in H.

Русский

Пусть H — подгруппа группы G. Тогда H сама является группой под той же операцией, и обратный элемент h^{-1} для любого h ∈ H принадлежит H.

LaTeX

$$$H \le G \\Rightarrow \\forall h \in H,\ h^{-1} \in H$$$

Lean4

/-- A subgroup of a group inherits an inverse. -/
@[to_additive /-- An `AddSubgroup` of an `AddGroup` inherits an inverse. -/
    ]
instance inv : Inv H :=
  ⟨fun a => ⟨a⁻¹, H.inv_mem a.2⟩⟩

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