ofRatRingHom — Mathlib

English

The construction of ofRat extends to a ring hom from β into CauSeq.Completion.Cauchy abv.

Русский

Конструкция ofRat распространяется на гомоморф кольца от β в CauSeq.Completion.Cauchy abv.

LaTeX

$$$\operatorname{ofRat}: \beta \to \mathrm{CauSeq.Completion.Cauchy}\ abv$ extends to a ring hom.$$

Lean4

/-- `CauSeq.Completion.ofRat` as a `RingHom` -/
@[simps]
def ofRatRingHom : β →+* (Cauchy abv) where
  toFun := ofRat
  map_zero' := ofRat_zero
  map_one' := ofRat_one
  map_add' := ofRat_add
  map_mul' := ofRat_mul

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