eq_inv_of_mul_eq_one_left

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.eq_inv_of_mul_eq_one_left

Lean4

protected theorem eq_inv_of_mul_eq_one_left (h : a * b = 1) : a = b⁻¹ :=
  by
  rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h, one_mul]
  rintro rfl
  simp [left_ne_zero_of_mul_eq_one h] at h

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

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

Разделы

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

Аффилиация

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