coe_one_eq_coeSubmodule_top — Mathlib

English

The underlying submodule of the unit fractional ideal equals the submodule corresponding to the top ideal.

Русский

Пусть подмодуль единичного дробного идеала равен подмодулю, соответствующему верхнему идеалу.

LaTeX

$$$\uparrow(1 : \mathrm{FractionalIdeal} S P) = \mathrm{coeSubmodule} P (\top : \mathrm{Ideal} R)$$$

Lean4

/-- `(1 : FractionalIdeal S P)` is defined as the R-submodule `f(R) ≤ P`.

However, this is not definitionally equal to `1 : Submodule R P`,
which is proved in the actual `simp` lemma `coe_one`. -/
theorem coe_one_eq_coeSubmodule_top : ↑(1 : FractionalIdeal S P) = coeSubmodule P (⊤ : Ideal R) :=
  rfl

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