div

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.div

English

If t ~_l u and v ~_l w, then t / v ~_l u / w.

Русский

Если t ~_l u и v ~_l w, то t / v ~_l u / w.

LaTeX

$$$ (t \\sim_{l} u) \\land (v \\sim_{l} w) \\Rightarrow (t / v) \\sim_{l} (u / w) $$$

Lean4

protected theorem div (htu : t ~[l] u) (hvw : v ~[l] w) : t / v ~[l] u / w := by
  simpa only [div_eq_mul_inv] using htu.mul hvw.inv

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

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

Разделы

Аффилиация

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