toLinearMap_apply

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.toLinearMap_apply

English

Applying the linear map underlying an algebra equivalence to an element x yields the value of the equivalence on x.

Русский

Применение линейного отображения эквивалентности к элементу x даёт изображение x этой эквивалентности.

LaTeX

$$$e^{\\text{toLinearMap}}(x) = e(x)$$$

Lean4

@[simp]
theorem toLinearMap_apply (x : A₁) : e.toLinearMap x = e x :=
  rfl

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

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

Разделы

Аффилиация

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