isIntegral_iff — Mathlib

English

For x ∈ S, IsIntegral K x ↔ IsIntegral K x.val with x : S; i.e., integrality is preserved under the inclusion S ↪ L.

Русский

Для x ∈ S: IsIntegral K x ⇔ IsIntegral K x. При включении S ⊆ L сохраняется интегральность.

LaTeX

$$$ IsIntegral\_K\; x \;\iff\; IsIntegral\_K\; x^{\text{val}} $$$

Lean4

theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) :=
  (isIntegral_algHom_iff S.val S.val.injective).symm

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