comp_smul — Mathlib

English

For a ring hom f: R →+* S, a, b, c ∈ R, and u ∈ R, we have f ∘ (u • P) = (f u) • (f ∘ P).

Русский

Для гомоморфизма колец f: R →+* S, и для P: Fin 3 → R, выполняется f ∘ (u • P) = (f u) • (f ∘ P).

LaTeX

$$$f \circ (u \cdot P) = (f u) \cdot (f \circ P)$$$

Lean4

theorem comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f u • f ∘ P := by ext n;
  fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp

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