comp_smul — Mathlib

English

For any RingHom f: R →+* S, P: Fin 3 → R, and u ∈ R, the equality f ∘ (u • P) = (f u) • (f ∘ P) holds, i.e., scalar action commutes with ring homomorphisms componentwise.

Русский

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

LaTeX

$$f ∘ (u • P) = f u • (f ∘ 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

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