finAddFlip_apply_castAdd — Mathlib

English

Applying the rotation to a casted addition yields the expected result: finAddFlip (Fin.castAdd n k) = Fin.natAdd n k.

Русский

Применение поворота к сложению через castAdd даёт ожидаемый результат: finAddFlip (Fin.castAdd n k) = Fin.natAdd n k.

LaTeX

$$$ finAddFlip (Fin.castAdd n k) = Fin.natAdd n k $$$

Lean4

@[simp]
theorem finAddFlip_apply_castAdd (k : Fin m) (n : ℕ) : finAddFlip (Fin.castAdd n k) = Fin.natAdd n k := by
  simp [finAddFlip]

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