coe_ne_zero_iff — Mathlib

English

Let K be a field and 𝓞_K its ring of integers. The natural map from 𝓞_K to K is injective.

Русский

Пусть K — поле и 𝓞_K — его кольцо целых. Естественное вложение 𝓞_K в K инъективно.

LaTeX

$$$\\operatorname{Injective}\\big(\\mathrm{algebraMap}_{\\mathcal{O}_K \\to K}\\big)$$$

Lean4

/-- The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `map_ne_zero_iff` applied to
`FaithfulSMul.algebraMap_injective`.
-/
theorem coe_ne_zero_iff {x : 𝓞 K} : algebraMap _ K x ≠ 0 ↔ x ≠ 0 :=
  map_ne_zero_iff _ coe_injective

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