coe_coeIdeal — Mathlib

English

For any I, the underlying submodule of the fractional ideal I produced by coeIdeal, when viewed as a submodule, equals the submodule associated to I by the standard construction.

Русский

Для любого I, подмодульная основа дробного идеала, полученного через coeIdeal, равна обычному подмодулю, ассоциированному с I.

LaTeX

$$$((I : FractionalIdeal\ S\ P) : Submodule R P) = coeSubmodule P I$$

Lean4

@[simp, norm_cast]
theorem coe_coeIdeal (I : Ideal R) : ((I : FractionalIdeal S P) : Submodule R P) = coeSubmodule P I :=
  rfl

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