mk_eq

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.mk_eq

English

Two Padic sequences f and g satisfy mk f = mk g iff f ≈ g.

Русский

Две последовательности Padic f и g удовлетворяют mk f = mk g тогда и только тогда, когда f ≈ g.

LaTeX

$$$\\mathrm{Padic.mk}(f) = \\mathrm{Padic.mk}(g) \\iff f \\approx g$$$

Lean4

theorem mk_eq {f g : PadicSeq p} : mk f = mk g ↔ f ≈ g :=
  Quotient.eq'

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

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

Разделы

Аффилиация

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