divp_eq_div

Mathlib.Algebra.Group.Units.Defs

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

English

For a and a unit u, the divp operation equals the usual division: a /ₚ u = a / u.

Русский

Для a и единицы u операция divp совпадает с обычным делением: a /ₚ u = a / u.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] (a : \alpha) (u : \alpha^×), a /_{p} u = a / u$$$

Lean4

theorem divp_eq_div [DivisionMonoid α] (a : α) (u : αˣ) : a /ₚ u = a / u := by
  rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]

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

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

Разделы

Аффилиация

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