ofRat_mul — Mathlib

English

For any x, y in β, the image of the product equals the product of the images: the embedding preserves multiplication.

Русский

Пусть x, y ∈ β. Образ произведения равен произведению образов: вложение сохраняет умножение.

LaTeX

$$$\operatorname{ofRat}(x \cdot y) = (\operatorname{ofRat}x \cdot \operatorname{ofRat}y : \mathrm{CauSeq.Completion.Cauchy}\,abv)$$$

Lean4

theorem ofRat_mul (x y : β) : ofRat (x * y) = (ofRat x * ofRat y : Cauchy abv) :=
  congr_arg mk (const_mul _ _)

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