coe_mk — Mathlib

English

For a fractional ideal I (regarded as a submodule of P), the canonical coercion to a submodule is the identity on I: the underlying submodule is exactly I.

Русский

Для дробного идеала I, рассматриваемого как подмодуль P, каноническое отображение в подмодуль даёт тот же самый подмодуль: его основанный подмодуль равен I.

LaTeX

$$$\mathrm{coeToSubmodule}\langle I, hI\rangle = I$$$

Lean4

@[simp, norm_cast]
theorem coe_mk (I : Submodule R P) (hI : IsFractional S I) : coeToSubmodule ⟨I, hI⟩ = I :=
  rfl

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