divp_inv

Mathlib.Algebra.Group.Units.Defs

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

English

Dividing by the inverse of a unit is equivalent to multiplying by the unit: a /ₚ u⁻¹ = a · u.

Русский

Деление на обратное единице равно умножению на единицу: a /ₚ u⁻¹ = a · u.

LaTeX

$$$a /ₚ u^{-1} = a \cdot u$$$

Lean4

@[simp]
theorem divp_inv (u : αˣ) : a /ₚ u⁻¹ = a * u :=
  rfl

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

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

Разделы

Аффилиация

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