Theorems · Theorem · commutative algebra

IsIntegral.tower_bot_of_field

∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommRing R] [inst_1 : Field A] [inst_2 : Ring B] [Nontrivial B]
  [inst_4 : Algebra R A] [inst_5 : Algebra A B] [inst_6 : Algebra R B] [IsScalarTower R A B] {x : A},
  IsIntegral R ((algebraMap A B) x) → IsIntegral R x

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFieldRingNontrivialAlgebraAlgebraAlgebraIsScalarTower