equiv_ι — Mathlib

English

Under the equivalence, the generator ι maps to the scalar ε in the dual-number ring: ι ↦ ε.

Русский

При переходе через эквивиаленту генератор ι отображается в ε в дуальном кольце: ι ↦ ε.

LaTeX

$$$\text{equiv}(\iota) = \varepsilon$$$

Lean4

@[simp]
theorem equiv_ι (r : R) : CliffordAlgebraDualNumber.equiv (ι (R := R) _ r) = r • ε :=
  (lift_ι_apply _ _ r).trans (inr_eq_smul_eps _)

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