isIntegral_sup — Mathlib

English

Let S and T be subalgebras of A over R. Then the join S ⊔ T is integral over R if and only if both S and T are integral over R.

Русский

Пусть S и T — подалгебры над R внутри A. Тогда их сумма (объединение) S ⊔ T интегральна над R тогда и только тогда, когда и S, и T интегральны над R.

LaTeX

$$$IsIntegral R (S \sqcup T) \iff IsIntegral R S \land IsIntegral R T$$$

Lean4

theorem isIntegral_sup {S T : Subalgebra R A} :
    Algebra.IsIntegral R (S ⊔ T : Subalgebra R A) ↔ Algebra.IsIntegral R S ∧ Algebra.IsIntegral R T := by
  simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]

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