coe_toPrincipalIdeal — Mathlib

English

For the unit x in K, the underlying monoid hom sends x to the principal fractional ideal generated by x.

Русский

Для единицы x в K соответствующее отображение переводит x в главный фракционный идеал, порождаемый x.

LaTeX

$$coe_toPrincipalIdeal (x) : (toPrincipalIdeal R K x) = spanSingleton _ (x)$$

Lean4

@[simp]
theorem coe_toPrincipalIdeal (x : Kˣ) : (toPrincipalIdeal R K x : FractionalIdeal R⁰ K) = spanSingleton _ (x : K) := by
  simp only [toPrincipalIdeal]; rfl

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