coe_val_mul_coe_inv_val

Mathlib.Algebra.Group.Submonoid.Units

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

← MathLib Explorer

English

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

Русский

Для S ⊆ M и x ∈ Sˣ: ((x) в M) * ((x⁻¹) в M) = 1.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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