div_ne_one_of_ne

Mathlib.Algebra.Group.Basic

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

English

If a ≠ b, then a / b ≠ 1.

Русский

Если a ≠ b, то a / b ≠ 1.

LaTeX

$$$\forall a,b\in G,\ a \neq b \Rightarrow a/b \neq 1$$$

Lean4

@[to_additive]
theorem div_ne_one_of_ne : a ≠ b → a / b ≠ 1 :=
  mt eq_of_div_eq_one

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

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

Разделы

Аффилиация

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