smul_right_iff₀ — Mathlib

English

If a ≠ 0, then x commutes with a • y if and only if x commutes with y, given SMulCommClass and IsScalarTower conditions.

Русский

При a ≠ 0 верно: x коммутирует с a • y тогда и только тогда, когда x коммутирует с y, при условии SMulCommClass и IsScalarTower.

LaTeX

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

Lean4

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

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