coe_injective — Mathlib

English

The natural inclusion of units of 𝓞K into K is injective; distinct units map to distinct elements of K.

Русский

Естественное включение единиц 𝓞K в K инъективно; различные единицы переходят в разные элементы K.

LaTeX

$$Injective(i: (𝓞K)^{×} → K)$$

Lean4

theorem coe_injective : Function.Injective ((↑) : (𝓞 K)ˣ → K) :=
  RingOfIntegers.coe_injective.comp Units.val_injective

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