Theorems · Definition · commutative algebra

Ideal.Quotient.factorPow

{R : Type u_1} → [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → {m n : ℕ} → n ≤ m → R ⧸ I ^ m →+* R ⧸ I ^ n

The ring homomorphism from R ⧸ I ^ m to R ⧸ I ^ n induced by the natural inclusion I ^ n → I ^ m. To future contributors: Before adding lemmas related to Ideal.factorPow, please check whether it can be generalized to Ideal.factor and whether the corresponding (more general) lemma for Ideal.factor already exists.

Defined in

Mathlib.RingTheory.Ideal.Quotient.PowTransition

Cited by

18 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSided