coe_inv — Mathlib

English

For a group G and submonoid S ⊆ G, the underlying set of the inverse submonoid S⁻¹ is the inverse of the underlying set of S: ↑(S⁻¹) = (S)⁻¹.

Русский

Пусть G — группа и S — подмономоид. Тогда множество S⁻¹ как подмономоид эквивалентно множеству обратных элементов: ↑(S⁻¹) = (S)⁻¹.

LaTeX

$$$\\uparrow(S^{-1}) = (S^{-1} : \\mathrm{Set} G) = (S : \\mathrm{Set} G)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_inv (S : Submonoid G) : ↑S⁻¹ = (S : Set G)⁻¹ :=
  rfl

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