mul_apply'

Mathlib.Algebra.Algebra.Bilinear

URI: https://scilib.ai/kg/mathlib#LinearMap.mul_apply'

English

Left multiplication by a is injective: mulLeft R a = mulLeft R b implies a = b (under SMulCommClass).

Русский

Умножение слева на a является инъективным: mulLeft R a = mulLeft R b ⇒ a = b (при SMulCommClass).

LaTeX

$$$$ mulLeft R a = mulLeft R b \;\iff\; a = b. $$$$

Lean4

@[simp]
theorem mul_apply' (a b : A) : mul R A a b = a * b :=
  rfl

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

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

Разделы

Аффилиация

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