mulRight_eq_zero_iff

Mathlib.Algebra.Algebra.Bilinear

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

English

Right multiplication by a equals zero iff a = 0: mulRight R a = 0 ⇔ a = 0 (under IsScalarTower).

Русский

Правое умножение на a равно нулю тогда и только тогда, когда a = 0 (при IsScalarTower).

LaTeX

$$$$ mulRight R a = 0 \iff a = 0. $$$$

Lean4

@[simp]
theorem mulRight_eq_zero_iff (a : A) : mulRight R a = 0 ↔ a = 0 :=
  mulRight_zero_eq_zero R A ▸ mulRight_inj

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

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

Разделы

Аффилиация

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