mulEquiv_apply

Mathlib.Algebra.Group.TransferInstance

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

English

The underlying function of mulEquiv e is just e on elements: (mulEquiv e) a = e(a).

Русский

Пусть mulEquiv e — мультиэквивалентность; её основанная функция совпадает с e: (mulEquiv e) a = e(a).

LaTeX

$$$$ (\\mathrm{mulEquiv}\\ e)\, a = e(a). $$$$

Lean4

@[to_additive (attr := simp)]
theorem mulEquiv_apply (e : α ≃ β) [Mul β] (a : α) : (mulEquiv e) a = e a :=
  rfl

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

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

Разделы

Аффилиация

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