mulEquiv_symm_apply

Mathlib.Algebra.Group.TransferInstance

URI: https://scilib.ai/kg/mathlib#Equiv.mulEquiv_symm_apply

English

The inverse of mulEquiv e acts as e^{-1} on β: (mulEquiv e).symm b = e^{-1}(b).

Русский

Обратная к mulEquiv e действует как e^{-1} на β: (mulEquiv e).symm b = e^{-1}(b).

LaTeX

$$$$ (\\mathrm{MulEquiv}\\ e).\\mathrm{symm}\ b = e^{-1}(b). $$$$

Lean4

@[to_additive]
theorem mulEquiv_symm_apply (e : α ≃ β) [Mul β] (b : β) :
    letI := Equiv.mul e
    (mulEquiv e).symm b = e.symm b :=
  rfl

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

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

Разделы

Аффилиация

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