isIntegral_of_surjective — Mathlib

English

If R → S → T is a tower with integrality conditions, then integrality descends from T to R via the composed maps.

Русский

Если R → S → T — башня с условиями интегральности, то интегральность спускается по композиции отображений.

LaTeX

$$$\text{tower_bot}$$$

Lean4

theorem isIntegral_of_surjective (hf : Function.Surjective f) : f.IsIntegral := fun x ↦
  (hf x).recOn fun _y hy ↦ hy ▸ f.isIntegralElem_map

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