map_isIntegral_int — Mathlib

English

If b is integral over ℤ, then its image under any ring hom f: B → C is still integral over ℤ.

Русский

Если b интегрален над ℤ, то образ f(b) в C также интегрален над ℤ.

LaTeX

$$$\\text{IsIntegral}_\\mathbb{Z}(f(b))$$$

Lean4

theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B} [FunLike F B C] [RingHomClass F B C] (f : F)
    (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) :=
  hb.map (f : B →+* C).toIntAlgHom

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