ofRat_div

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.ofRat_div

English

The image of x / y equals the quotient of the images, i.e., ofRat(x/y) = ofRat(x) / ofRat(y).

Русский

Образ x/y равен частному образов: ofRat(x/y) = ofRat(x) / ofRat(y).

LaTeX

$$$\operatorname{ofRat}(x / y) = (\operatorname{ofRat} x / \operatorname{ofRat} y : \mathrm{CauSeq abv})$$$

Lean4

theorem ofRat_div (x y : β) : ofRat (x / y) = (ofRat x / ofRat y : Cauchy abv) := by
  simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]

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

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

Разделы

Аффилиация

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