smul_left_iff₀ — Mathlib

English

If a ≠ 0, then a • x commutes with y iff x commutes with y, under appropriate SMul classes.

Русский

Если a ≠ 0, то a • x коммутирует с y тогда и только тогда, когда x коммутирует с y.

LaTeX

$$$\\text{Commute}(a \\cdot x, y) \\iff \\text{Commute}(x, y)$$$

Lean4

@[simp]
theorem smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) :
    Commute (a • x) y ↔ Commute x y :=
  Commute.smul_left_iff (g := Units.mk0 a ha)

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