iterToSum_C_C — Mathlib

English

Applying iterToSum to the constant double embedding C(C a) yields the single constant embedding C a.

Русский

Применение iterToSum к константному двойному внедрению C(C a) дает константное внедрение C a.

LaTeX

$$$\operatorname{iterToSum} \;R\;S_1\;S_2\bigl(C(C a)\bigr) = C a$$$

Lean4

@[simp]
theorem iterToSum_C_C (a : R) : iterToSum R S₁ S₂ (C (C a)) = C a :=
  Eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)

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