algebra — Mathlib

English

There is a natural algebra structure on the product ∏_i A_i, defined pointwise, making it an Algebra over R.

Русский

На произведении ∏_i A_i существует естественная структура алгебры, задаваемая по точкам, делающая произведение алгеброй над R.

LaTeX

$$$ \\text{Algebra } R (\\prod_i A_i) \\text{ with canonical pointwise operations} $$$

Lean4

instance algebra : Algebra R (Π i, A i)
    where
  algebraMap := Pi.ringHom fun i ↦ algebraMap R (A i)
  commutes' := fun a f ↦ by ext; simp [Algebra.commutes]
  smul_def' := fun a f ↦ by ext; simp [Algebra.smul_def]

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