ringEquiv_apply

Mathlib.Algebra.Ring.TransferInstance

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

English

For a ring equivalence induced by e, applying it to an element a yields the image e(a).

Русский

Для кольцевой эквивалентности, порождённой e, применение к элементу a даёт образ e(a).

LaTeX

$$$(\text{ringEquiv } e)(a) = e(a)$$$

Lean4

@[simp]
theorem ringEquiv_apply (e : α ≃ β) [Add β] [Mul β] (a : α) : ringEquiv e a = e a :=
  rfl

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

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

Разделы

Аффилиация

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