∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_3) [inst_1 : Field L]
  [inst_2 : Algebra K L] (E : Type u_2) [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : Algebra L E]
  [IsScalarTower K L E], IsIntegral (↥v.valuationSubring) ((algebraMap L E) ↑0)