inr_eq_smul_eps

Mathlib.Algebra.DualNumber

URI: https://scilib.ai/kg/mathlib#DualNumber.inr_eq_smul_eps

English

The inr embedding sends r to r times ε.

Русский

Встраивание inr отображает r в r·ε.

LaTeX

$$$\text{inr}(r) = r \cdot \varepsilon$$$

Lean4

@[simp]
theorem inr_eq_smul_eps [MulZeroOneClass R] (r : R) : inr r = (r • ε : R[ε]) :=
  ext (mul_zero r).symm (mul_one r).symm

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

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

Разделы

Аффилиация

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