integralClosure_eq_top_iff — Mathlib

English

The integral closure equals the top subalgebra iff A is integral over R.

Русский

Интегральное замыкание равно вершинной подалгебре тогда и только тогда, когда A интегральна над R.

LaTeX

$$$integralClosure R A = \\top \\iff Algebra.IsIntegral R A$$$

Lean4

theorem integralClosure_eq_top_iff : integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A := by
  rw [← top_le_iff, le_integralClosure_iff_isIntegral, (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]
    -- explicit arguments for speedup

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