relabelAux_sumInl — Mathlib

English

Relabeling with Sum.inl coincides with a standard Sum.map on finite additions.

Русский

Перелепление через Sum.inl совпадает с обычным Sum.map для суммирования над Fin.

LaTeX

$$$relabelAux (Sum.inl : α → α ⊕ (Fin n)) k = Sum.map id (natAdd n).$$$

Lean4

@[simp]
theorem relabelAux_sumInl (k : ℕ) : relabelAux (Sum.inl : α → α ⊕ (Fin n)) k = Sum.map id (natAdd n) :=
  by
  ext x
  cases x <;> · simp [relabelAux]

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