pnatCast — Mathlib

English

A canonical map from positive naturals to units of R is defined, compatible with equality of naturals.

Русский

Определено каноническое отображение из положительных натуральных чисел в едииницы кольца R, совместимое с равенством чисел.

LaTeX

$$$\\text{pnatCast}: \\mathbb{N}_{>0} \\to \\mathrm{Units}(R)$$$

Lean4

@[coe]
noncomputable def pnatCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ℕ+ → Rˣ := fun n =>
  (PNat.isUnit_natCast n).unit

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