algEquivQuotient_symm_apply — Mathlib

English

The symmetric action of the quotient isomorphism is given by an explicit expression involving the mod' of the quotient equivalence; applying the inverse map to a quotient class yields that expression.

Русский

Симметричное отображение изоморфизма деления задаётся явным выражением через mod'. Применение обратного отображения к классу в (PowerSeries) даёт это выражение.

LaTeX

$$The inverse of the quotient isomorphism sends x to the class of the mod' expression derived from the quotient equivalence of A via g.$$

Lean4

@[simp]
theorem algEquivQuotient_symm_apply [IsAdicComplete I A] (x : A⟦X⟧ ⧸ Ideal.span { g }) :
    H.algEquivQuotient.symm x =
      Ideal.Quotient.mk _
        (H.isDistinguishedAt.isWeierstrassDivisorAt'.mod' <|
          Ideal.quotientEquivAlgOfEq A (by rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]) x) :=
  by simp [algEquivQuotient]

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