coeToSet_coeToSubmodule — Mathlib

English

For any fractional ideal I, its set-theoretic representation as a subset of P coincides with I itself when viewed as a fractional ideal.

Русский

Для дробного идеала I множество элементов, воспринимаемое как подмножество P, совпадает с самим I.

LaTeX

$$$((I : \mathrm Submodule\ R\ P) : \mathrm Set\ P) = I$$$

Lean4

theorem coeToSet_coeToSubmodule (I : FractionalIdeal S P) : ((I : Submodule R P) : Set P) = I :=
  rfl

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