tensorProduct — Mathlib

English

The tensor product of two integral algebras over R is integral over R.

Русский

Тензорное произведение двух интегральных алгебр над R является интегральной над R.

LaTeX

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

Lean4

instance tensorProduct [CommRing B] [Algebra R A] [Algebra R B] [int : Algebra.IsIntegral R B] :
    Algebra.IsIntegral A (A ⊗[R] B) where
  isIntegral p := p.induction_on isIntegral_zero (fun _ s ↦ .tmul _ <| int.1 s) (fun _ _ ↦ .add)

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