smul_equiv_smul — Mathlib

English

If f1 ≈ f2 then for any scalar action, c • f1 ≈ c • f2.

Русский

Если f1 ≈ f2, то для любого скалярного действия c • f1 ≈ c • f2.

LaTeX

$$$ c \cdot f_1 \approx c \cdot f_2 $$$

Lean4

theorem smul_equiv_smul {G : Type*} [SMul G β] [IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G) (hf : f1 ≈ f2) :
    c • f1 ≈ c • f2 := by
  simpa [const_smul, smul_one_mul _ _] using mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf

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