right_eq_zero_of_smul

Mathlib.Algebra.Regular.SMul

URI: https://scilib.ai/kg/mathlib#IsSMulRegular.right_eq_zero_of_smul

← MathLib Explorer

English

If IsSMulRegular M r holds and r • x = 0, then x = 0.

Русский

Если выполнено IsSMulRegular M r и r • x = 0, то x = 0.

LaTeX

$$$IsSMulRegular M r \Rightarrow (r \cdot x = 0 \Rightarrow x = 0)$$$

Lean4

protected theorem right_eq_zero_of_smul [Zero M] [SMulZeroClass R M] {r : R} {x : M} (h1 : IsSMulRegular M r)
    (h2 : r • x = 0) : x = 0 :=
  h1 (h2.trans (smul_zero r).symm)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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