pair_iff — Mathlib

English

For x in A×B, IsIntegral R x holds exactly when x's first and second components are integral over R.

Русский

Для x = (a,b) в A×B: IsIntegral R x эквивалентно IsIntegral R a и IsIntegral R b.

LaTeX

$$$\\text{IsIntegral}_R((a,b)) \\iff (\\text{IsIntegral}_R(a) \\land \\text{IsIntegral}_R(b))$$$

Lean4

/-- An element of a product algebra is integral iff each component is integral. -/
theorem pair_iff {x : A × B} : IsIntegral R x ↔ IsIntegral R x.1 ∧ IsIntegral R x.2 :=
  ⟨fun h ↦ ⟨h.map (AlgHom.fst R A B), h.map (AlgHom.snd R A B)⟩, fun h ↦ h.1.pair h.2⟩

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