mk_intCast — Mathlib

English

Integers embed in the localization in the expected way: the image of an integer m under the localization construction is exactly m.

Русский

Целые числа естественным образом внедряются в локализацию: образ целого m под локализацией равен самому m.

LaTeX

$$$\\text{mk}_{\\mathbb{Z}}(m,1) = m \\quad (m \\in \\mathbb{Z})$$$

Lean4

theorem mk_intCast (m : ℤ) : (mk m 1 : Localization M) = m := by simpa using mk_algebraMap (R := R) (A := ℤ) _

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