mul_right_inj_of_invertible

Mathlib.Algebra.Group.Invertible.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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