coe_mk0 — Mathlib

English

The canonical embedding respects mk0, i.e., the image under mk0 in the ambient fractional ideal matches the original ideal.

Русский

Каноническое вложение сохраняет mk0: образ mk0 в окружающем дробном идеале совпадает с исходным идеалом.

LaTeX

$$$\mathrm{FractionalIdeal.mk0}(K,I)\;\text{coe}=I,$ where $I$ is an integral ideal.$$

Lean4

@[simp]
theorem coe_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) : (FractionalIdeal.mk0 K I : FractionalIdeal R⁰ K) = I :=
  rfl

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