eq_of_one_div_eq_one_div

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$1 / a = 1 / b \\Rightarrow a = b$$$

Lean4

@[to_additive]
theorem eq_of_one_div_eq_one_div (h : 1 / a = 1 / b) : a = b := by
  rw [← one_div_one_div a, h, one_div_one_div]
    -- Note that `mul_zsmul` and `zpow_mul` have the primes swapped
    -- when additivised since their argument order,
    -- and therefore the more "natural" choice of lemma, is reversed.

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

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

Разделы

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

Аффилиация

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