English
An element (a,b) of a product algebra A×B is integral over R if and only if a and b are integral over R.
Русский
Элемент (a,b) в произведении алгебр A×B интегральный над R тогда и только тогда, когда a и b интегральны над R.
LaTeX
$$$\\mathrm{IsIntegral}_R((a,b))\\;\\text{ iff }\\mathrm{IsIntegral}_R(a) \\land \\mathrm{IsIntegral}_R(b)$$$
Lean4
/-- An element of a product algebra is integral if each component is integral. -/
theorem pair {x : A × B} (hx₁ : IsIntegral R x.1) (hx₂ : IsIntegral R x.2) : IsIntegral R x :=
by
obtain ⟨p₁, ⟨hp₁Monic, hp₁Eval⟩⟩ := hx₁
obtain ⟨p₂, ⟨hp₂Monic, hp₂Eval⟩⟩ := hx₂
refine ⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩
rw [← aeval_def] at *
rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero, Prod.zero_eq_mk]
