mulLeft_one

Mathlib.Algebra.Algebra.Bilinear

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

English

The bilinear map mul satisfies mul a b = a b for all a,b in A.

Русский

Билинейная карта mul удовлетворяет mul a b = a b для всех a,b ∈ A.

LaTeX

$$$$ mul\,R\,A\,a\,b = a b. $$$$

Lean4

@[simp]
theorem mulLeft_one : mulLeft R (1 : A) = LinearMap.id :=
  ext fun _ => one_mul _

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

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

Разделы

Аффилиация

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