coe_ringOfIntegersEquiv — Mathlib

English

Under the equivalence between 𝓞ℚ and ℤ, the natural embedding agrees with the standard algebra map.

Русский

При эквивалентности 𝓞ℚ ≃ ℤ соответствие вложения совпадает с обычной алгебраической картой.

LaTeX

$$$(Rat.ringOfIntegersEquiv z : \\mathbb{Q}) = \\text{algebraMap}(\\mathcal{O}_{\\mathbb{Q}} \\to \\mathbb{Q})\, z$ for $z\\in 𝓞\\mathbb{Q}$.$$

Lean4

@[simp]
theorem coe_ringOfIntegersEquiv (z : 𝓞 ℚ) : (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z :=
  by
  obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
  simp

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