smulOfRingMorphism_smul_eq' — Mathlib

English

In the same setting as above, the right action is given by a • f = f ≫ (φ(a)).app Y, i.e., the endomorphism at Y postcomposes with f.

Русский

В той же постановке слева действие кольца выражается как a • f = f ≫ (φ(a)).app Y, то есть эндоморфизм на Y домножает справа на f.

LaTeX

$$$a \cdot f = f \circ (\phi(a))_{Y}$$$

Lean4

/-- `a • f = f ≫ (φ a).app Y`. -/
theorem smulOfRingMorphism_smul_eq' (a : R) (f : X ⟶ Y) :
    letI := smulOfRingMorphism φ X Y
    a • f = f ≫ (φ a).app Y :=
  by
  rw [smulOfRingMorphism_smul_eq]
  exact ((φ a).naturality f).symm

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