ringHom

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.Coe.ringHom

English

There is a canonical ring homomorphism from ℤ_p to ℚ_p given by the inclusion.

Русский

Существует канонический гомоморфизм колец из ℤ_p в ℚ_p, заданный включением.

LaTeX

$$$\text{ringHom}: \mathbb{Z}_p \to \mathbb{Q}_p \quad \text{is the inclusion}$$$

Lean4

/-- The coercion from `ℤ_[p]` to `ℚ_[p]` as a ring homomorphism. -/
def ringHom : ℤ_[p] →+* ℚ_[p] :=
  (subring p).subtype

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

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

Разделы

Аффилиация

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