prod — Mathlib

English

If A and B are integral algebras over R, then the product algebra A × B is integral over R.

Русский

Если A и B — интегральные алгебры над R, то произведение A × B является интегральной над R алгеброй.

LaTeX

$$$[\text{Algebra.IsIntegral } R A] \; [\text{Algebra.IsIntegral } R B] \Rightarrow \text{Algebra.IsIntegral } R (A \times B)$$$

Lean4

/-- Product of two integral algebras is an integral algebra. -/
instance prod [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] : Algebra.IsIntegral R (A × B) :=
  Algebra.isIntegral_def.mpr fun x ↦ (Algebra.isIntegral_def.mp ‹_› x.1).pair (Algebra.isIntegral_def.mp ‹_› x.2)

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