lift_inlAlgHom_eps — Mathlib

English

Lifting the canonical left-inclusion together with ε gives the identity on the dual-number extension.

Русский

Подъём канонической левой инъекции вместе с ε даёт тождественный отображение на A[ε].

LaTeX

$$lift ⟨(inlAlgHom R A A, ε), eps_mul_eps, fun _ => commute_eps_left _⟩ = AlgHom.id R A[ε]$$

Lean4

/-- Lifting `DualNumber.eps` itself gives the identity. -/
@[simp]
theorem lift_inlAlgHom_eps : lift ⟨(inlAlgHom _ _ _, ε), eps_mul_eps, fun _ => commute_eps_left _⟩ = AlgHom.id R A[ε] :=
  lift.apply_symm_apply <| AlgHom.id R A[ε]

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