Integral elements modulo powers of two-sided ideals

A monic relation modulo a two-sided ideal I gives a monic relation modulo every power I^n: raise the original polynomial to the n-th power. This works in noncommutative algebras because polynomials in a single element with central coefficients can be evaluated multiplicatively. It allows finiteness arguments using integral generators to survive passage to smaller ideals.

theorem Ado.isIntegral_quotient_pow_of_isIntegral_quotient {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {I : Ideal A} [I.IsTwoSided] (x : A) (hx : IsIntegral R ((Ideal.Quotient.mk I) x)) (n : ℕ) : IsIntegral R ((Ideal.Quotient.mk (I ^ n)) x)

Integrality of an element modulo a two-sided ideal implies integrality modulo every power of that ideal. No commutativity of the ambient algebra is needed.