sigmaCongrRight_inv

Mathlib.Algebra.Group.End

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

← MathLib Explorer

English

The inverse of sigmaCongrRight F is sigmaCongrRight of F inverse: (sigmaCongrRight F)^{-1} = sigmaCongrRight (F)^{-1}.

Русский

Обратная к sigmaCongrRight F равна sigmaCongrRight (F)^{-1}.

LaTeX

$$$$(sigmaCongrRight F)^{-1} = sigmaCongrRight (F)^{-1}.$$$$

Lean4

@[simp]
theorem sigmaCongrRight_inv {α : Type*} {β : α → Type*} (F : ∀ a, Perm (β a)) :
    (sigmaCongrRight F)⁻¹ = sigmaCongrRight fun a => (F a)⁻¹ :=
  rfl

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

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

Разделы

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

Аффилиация

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