val_div_eq_divp

Mathlib.Algebra.Group.Units.Defs

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

English

The value of the quotient of units equals the divp of their values: ↑(u1 / u2) = ↑u1 /ₚ u2.

Русский

Значение частного единиц равняется частичному делению значений: ↑(u1 / u2) = ↑u1 /ₚ u2.

LaTeX

$$$\uparrow(u_1 / u_2) = \uparrow u_1 /ₚ u_2$$$

Lean4

theorem val_div_eq_divp (u₁ u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ /ₚ u₂ := by rw [divp, division_def, Units.val_mul]

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

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

Разделы

Аффилиация

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