mk_eq_mk — Mathlib

English

For m ≤ n, and r ∈ AdicCauchySequence, Quotient.mk(I^m)(r.val n) equals Quotient.mk(I^m)(r.val m).

Русский

Для m ≤ n и r ∈ AdicCauchySequence: Quotient.mk(I^m)(r.val n) = Quotient.mk(I^m)(r.val m).

LaTeX

$$Quotient.mk(I^m)(r.val n) = Quotient.mk(I^m)(r.val m)$$

Lean4

theorem mk_eq_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) :
    Ideal.Quotient.mk (I ^ m) (r.val n) = Ideal.Quotient.mk (I ^ m) (r.val m) :=
  by
  have h : I ^ m = I ^ m • ⊤ := by simp
  rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]
  exact (r.property hmn).symm

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