app_units_zsmul — Mathlib

English

If the scalar is a unit in integers, the equality holds with units as exponents.

Русский

Если множитель является единицей в целых числах, равенство сохраняется на уровне единиц.

LaTeX

$$$$ (n\\cdot\\alpha).\\text{app} X = n\\cdot (\\alpha.\\text{app} X) $$ for units n.$$

Lean4

@[simp]
theorem app_units_zsmul (X : C) (α : F ⟶ G) (n : ℤˣ) : (n • α).app X = n • α.app X := by apply app_zsmul

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