coeToSubmodule — Mathlib

English

The map that forgets the fractional data sends a fractional ideal to its underlying R-submodule.

Русский

Отображение, забывающее дробную структуру, переводит дробный идеал в его подмодуль над R.

LaTeX

$$$\\text{coToSubmodule}(I) = I.\\text{val}$$$

Lean4

/-- Map a fractional ideal `I` to a submodule by forgetting that `∃ a, a I ⊆ R`.

This implements the coercion `FractionalIdeal S P → Submodule R P`.
-/
@[coe]
def coeToSubmodule (I : FractionalIdeal S P) : Submodule R P :=
  I.val

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