quotEquivPowQuotPowSuccEquiv — Mathlib

English

A plain equivalence on quotients: R/I is equivalent to the quotient used by pow-quot-succ construction.

Русский

Чистая эквив между R/I и квотой, используемой в конструировании pow-quot-succ.

LaTeX

$$$(R \!\!\! / I) \equiv (I^n : \mathrm{Ideal} R) / (I • \top)$$$

Lean4

/-- For a principal ideal `I`, `R ⧸ I ≃ I ^ n ⧸ I ^ (n + 1)`. Supplied as a plain equiv to bypass
typeclass synthesis issues on complex `Module` goals.  To convert into a form
that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
`Ideal.powQuotPowSuccEquivMapMkPowSuccPow`. -/
noncomputable def quotEquivPowQuotPowSuccEquiv (h : I.IsPrincipal) (h' : I ≠ ⊥) (n : ℕ) :
    (R ⧸ I) ≃ (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
  quotEquivPowQuotPowSucc h h' n

Похожие утверждения