inv_mem_valueGroup

Mathlib.Algebra.GroupWithZero.Range

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.inv_mem_valueGroup

English

If b.1 lies in the range of f, then the inverse b^{-1} lies in valueGroup f.

Русский

Если b.1 лежит в образе f, то b^{-1} ∈ valueGroup f.

LaTeX

$$hb : b.1 ∈ range f → b^{-1} ∈ valueGroup f$$

Lean4

theorem inv_mem_valueGroup {b : Bˣ} (hb : b.1 ∈ range f) : b⁻¹ ∈ valueGroup f :=
  Subgroup.inv_mem _ (mem_valueGroup f hb)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru