English
There is a canonical linear map called factorPowSucc that realizes the natural surjection from M/(I^(n+1) • ⊤) to M/(I^n • ⊤).
Русский
Существует каноническое линейное отображение factorPowSucc, реализующее естественную сюръекцию из M/(I^(n+1) • ⊤) в M/(I^n • ⊤).
LaTeX
$$$\mathrm{factorPowSucc}\;: M/(I^{n+1}\cdot \top) \to M/(I^{n}\cdot \top)$$$
Lean4
/-- 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.
-/
abbrev factorPow {m n : ℕ} (le : n ≤ m) : R ⧸ I ^ m →+* R ⧸ I ^ n :=
factor (pow_le_pow_right le)
