smul_eq — Mathlib

English

For any a in R and morphisms f, g in the quotient, the action satisfies a • [f] = [a • f].

Русский

Для любого a в R и морфизмов f, g в квотиенте верно a • [f] = [a • f].

LaTeX

$$$a \\cdot [f] = [a \\cdot f]$$$

Lean4

@[simp]
theorem smul_eq (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y) (_ : r f₁ f₂), r (a • f₁) (a • f₂)) (a : R) {X Y : C}
    (f : X ⟶ Y) :
    letI := smul r hr
    a • (functor r).map f = (functor r).map (a • f) :=
  rfl

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