algEquiv_apply

Mathlib.Algebra.Algebra.TransferInstance

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

English

The underlying function of algEquiv R e on an element a ∈ α is simply e(a).

Русский

Базовая функция algEquiv R e на элементе a ∈ α равна e(a).

LaTeX

$$$\\\\big(\\\\mathrm{algEquiv}\\\\,R\\\\,e\\\\big) \\\\text{ applied to } a = e(a).$$$

Lean4

@[simp]
theorem algEquiv_apply (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a :=
  rfl

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

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

Разделы

Аффилиация

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