mulRight_inj — Mathlib

English

Right multiplication by a product equals the composition of right multiplications: mulRight R (a b) = (mulRight R b) ∘ (mulRight R a).

Русский

Правое умножение на произведение равно композиции правых умножений: mulRight R (a b) = (mulRight R b) ∘ (mulRight R a).

LaTeX

$$$$ mulRight R (a b) = (mulRight R b) \circ (mulRight R a). $$$$

Lean4

@[simp]
theorem mulRight_inj [IsScalarTower R A A] {a b : A} : mulRight R a = mulRight R b ↔ a = b :=
  ⟨fun h => by simpa using LinearMap.ext_iff.mp h 1, fun h => h ▸ rfl⟩

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