finAddFlip_apply_natAdd — Mathlib

English

Applying the rotation to a natural addition yields the casted addition: finAddFlip (Fin.natAdd m k) = Fin.castAdd m k.

Русский

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

LaTeX

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

Lean4

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

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