diff_inv

Mathlib.GroupTheory.Transfer

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

English

The inverse of the diff between S and T is the diff between T and S: (diff(ϕ,S,T))^{-1} = diff(ϕ,T,S).

Русский

Обратное к diff(ϕ,S,T) равно diff(ϕ,T,S): (diff(ϕ,S,T))^{-1} = diff(ϕ,T,S).

LaTeX

$$$\bigl(\operatorname{diff}(\varphi,S,T)\bigr)^{-1} = \operatorname{diff}(\varphi,T,S)$$$

Lean4

@[to_additive]
theorem diff_inv : (diff ϕ S T)⁻¹ = diff ϕ T S :=
  inv_eq_of_mul_eq_one_right <| (diff_mul_diff ϕ S T S).trans <| diff_self ϕ S

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

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

Разделы

Аффилиация

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