sumCongr_inv

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.sumCongr_inv

English

The inverse of sumCongr e f is sumCongr e^{-1} f^{-1}.

Русский

Обратная к sumCongr e f равна sumCongr e^{-1} f^{-1}.

LaTeX

$$$$(sumCongr\\ e\\ f)^{-1} = sumCongr\\ e^{-1}\\ f^{-1}.$$$$

Lean4

@[simp]
theorem sumCongr_inv {α β : Type*} (e : Perm α) (f : Perm β) : (sumCongr e f)⁻¹ = sumCongr e⁻¹ f⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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