mul_left_injective₀

Mathlib.Algebra.GroupWithZero.Defs

URI: https://scilib.ai/kg/mathlib#mul_left_injective₀

English

If b ≠ 0, then left multiplication by b is injective: a1 · b = a2 · b implies a1 = a2.

Русский

Если b ≠ 0, тогда левая умножение на b инъективно: a1 · b = a2 · b ⇒ a1 = a2.

LaTeX

$$$b \neq 0 \Rightarrow (a_1 b = a_2 b \Rightarrow a_1 = a_2)\quad (a_1,a_2,b \in M)$$$

Lean4

theorem mul_left_injective₀ (hb : b ≠ 0) : Function.Injective fun a => a * b := fun _ _ => mul_right_cancel₀ hb

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

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

Разделы

Аффилиация

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