mk_mod'_eq_self — Mathlib

English

The mk_mod' relation holds: the quotient-lifted mod' equals mod on any representative.

Русский

Отношение mk_mod' равно mod на любом представителе.

LaTeX

$$$ \\text{mk_mod'_eq_self} \\;(H) : \\text{mod'}(f) = \\text{mod}(f) \\text{ in the quotient}. $$$

Lean4

@[simp]
theorem mk_mod'_eq_self [IsAdicComplete I A] {f : A⟦X⟧ ⧸ Ideal.span { g }} :
    Ideal.Quotient.mk _ (H.mod' f : A⟦X⟧) = f :=
  by
  obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
  rw [mod'_mk_eq_mod, Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
  use H.div f
  rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.symm]

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