diff_self

Mathlib.GroupTheory.Transfer

URI: https://scilib.ai/kg/mathlib#Subgroup.leftTransversals.diff_self

English

The difference of a transversal with itself is the identity: diff(ϕ, T, T) = 1.

Русский

Разность одной и той же трансверсали с самой собой равна единице: diff(ϕ, T, T) = 1.

LaTeX

$$$\operatorname{diff}(\varphi,T,T) = 1$$$

Lean4

@[to_additive]
theorem diff_self : diff ϕ T T = 1 :=
  mul_eq_left.mp (diff_mul_diff ϕ T T T)

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

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

Разделы

Аффилиация

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