mulRight_apply

Mathlib.Algebra.Algebra.Bilinear

URI: https://scilib.ai/kg/mathlib#LinearMap.mulRight_apply

English

For all a,b ∈ A, applying mulRight with a to b yields b a; i.e., (mulRight R a)(b) = b a.

Русский

Для всех a,b ∈ A применение mulRight к a к элементу b даёт b a; то есть (mulRight R a)(b) = b a.

LaTeX

$$$$ \forall a,b \in A,\quad (mulRight\,R\,a)(b) = b a. $$$$

Lean4

@[simp]
theorem mulRight_apply (a b : A) : mulRight R a b = b * a :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru