coe_natCast — Mathlib

English

For every natural number n, the image of n in FractionalIdeal S P, when viewed as a Submodule of P over R, coincides with the standard copy of n as a submodule of P.

Русский

Для каждого натурального числа n образ n в FractionalIdeal S P, рассматривая как подмодуль над R в P, совпадает со стандартным подмодулем, порожденным n в P.

LaTeX

$$$((n : \mathrm{FractionalIdeal}(S,P)) : \mathrm{Submodule} \\ R \\ P) = n$$$

Lean4

theorem coe_natCast (n : ℕ) : ((n : FractionalIdeal S P) : Submodule R P) = n :=
  show ((n.unaryCast : FractionalIdeal S P) : Submodule R P) = n by induction n <;> simp [*, Nat.unaryCast]

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