pnatCast_eq_natCast — Mathlib

English

The image of a positive natural under pnatCast equals its natural cast in R.

Русский

Изображение положительного натурального числа через pnatCast равно его натуральному отображению в R.

LaTeX

$$$\\text{pnatCast}(n) = n^{\\#} \\text{ in } R$$$

Lean4

/-- Internal: Not intended to be used outside this local construction. -/
@[simp]
theorem pnatCast_eq_natCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] (n : ℕ+) : ((n : Rˣ) : R) = ↑n :=
  by
  change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
  simp only [IsUnit.unit_spec]

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