Theorems · Theorem · commutative algebra

IsIntegral.map_of_comp_eq

∀ {R : Type u_5} {S : Type u_6} {T : Type u_7} {U : Type u_8} [inst : CommRing R] [inst_1 : Ring S]
  [inst_2 : CommRing T] [inst_3 : Ring U] [inst_4 : Algebra R S] [inst_5 : Algebra T U] (φ : R →+* T) (ψ : S →+* U),
  (algebraMap T U).comp φ = ψ.comp (algebraMap R S) → ∀ {a : S}, IsIntegral R a → IsIntegral T (ψ a)

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Cited by

2 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingCommRingRingAlgebraAlgebra