instRingMixedSpace — Mathlib

English

The mixed space carries a natural ring structure defined componentwise from the underlying real and complex parts.

Русский

Смешанное пространство обладает естественной структурой кольца, задаваемой по компонентам на основе соответствующих вещественных и комплексных частей.

LaTeX

$$Кольцо на смешанном пространстве задаётся координатно как произведение колец: координатное произведение операцией сложения и умножения.$$

Lean4

instance : Ring (euclidean.mixedSpace K) :=
  have : Ring (EuclideanSpace ℝ { w : InfinitePlace K // IsReal w }) := Pi.ring
  have : Ring (EuclideanSpace ℂ { w : InfinitePlace K // IsComplex w }) := Pi.ring
  inferInstanceAs (Ring (_ × _))

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