evalₐ_mkₐ

Mathlib.RingTheory.AdicCompletion.Algebra

URI: https://scilib.ai/kg/mathlib#AdicCompletion.evalₐ_mkₐ

English

There is a₁ compatibility: evalₐ I n (mkₐ I x) equals Quotient.mk(I^n)(x.val n).

Русский

Согласованность evalₐ с mkₐ: evalₐ I n (mkₐ I x) = Quotient.mk(I^n)(x.val n).

LaTeX

$$evalₐ(I,n)(mkₐ(I,x)) = Quotient.mk(I^n)(x.val n)$$

Lean4

@[simp]
theorem evalₐ_mkₐ (n : ℕ) (x : AdicCauchySequence I R) : evalₐ I n (mkₐ I x) = Ideal.Quotient.mk (I ^ n) (x.val n) := by
  simp [mkₐ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru