smul_left_iff — Mathlib

English

Same as inv_smul_eq_iff but stated in a slightly different form within commutative contexts.

Русский

То же самое, что и inv_smul_eq_iff, сформулированное в немного другой форме в рамках контекстов коммутативности.

LaTeX

$$$\\\\forall G \\\\in Group, \\\\forall a \\\\in α, \\\\forall g \\\\in G, \\\\ Eq a (g^{-1} \\\\cdot b) \\\\iff Eq (g \\\\cdot a) b.$$$

Lean4

@[simp]
theorem smul_left_iff : Commute (g • a) b ↔ Commute a b := by
  rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]

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