coe_inv_val_mul_coe_val

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Submonoid.coe_inv_val_mul_coe_val

← MathLib Explorer

English

For S a Submonoid of M and x ∈ Sˣ, ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1.

Русский

Для S ⊆ M и x ∈ Sˣ выполняется ((x⁻¹) : M) * ((x) : M) = 1.

LaTeX

$$$((x^{-1} : S^{\\times}) : M) \\cdot ((x : S^{\\times}) : M) = 1$$

Lean4

@[to_additive]
theorem coe_inv_val_mul_coe_val (S : Submonoid M) {x : Sˣ} : ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1 :=
  DFunLike.congr_arg S.subtype x.inv_mul

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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