lift_apply_eps — Mathlib

English

The lift sends the nilpotent coordinate ε to the element e in B.

Русский

Лифт отправляет ε в элемент e в B.

LaTeX

$$$\text{lift } fe (\varepsilon) = fe.2$$$

Lean4

/-- When applied to `ε`, `DualNumber.lift` produces the element of `B` that squares to 0. -/
@[simp]
theorem lift_apply_eps (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a) }) :
    lift fe (ε : A[ε]) = fe.val.2 := by
  simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, map_one, one_mul, zero_add]

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