mul_left_inj_of_invertible

Mathlib.Algebra.Group.Invertible.Defs

URI: https://scilib.ai/kg/mathlib#mul_left_inj_of_invertible

English

If c is invertible, then c*a = c*b iff a=b.

Русский

Если c обратимо, то c*a = c*b эквивалентно a=b.

LaTeX

$$$\\forall a,b\\in\\alpha,\\ (c*a = c*b) \\iff (a=b)$$$

Lean4

theorem mul_left_inj_of_invertible : a * c = b * c ↔ a = b :=
  ⟨fun h => by simpa using congr_arg (· * ⅟c) h, congr_arg (· * _)⟩

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

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

Разделы

Аффилиация

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