English
The value of pnatCast at 1 is the multiplicative identity in R.
Русский
Значение pnatCast на 1 равно единице умножения в R.
LaTeX
$$$\\text{pnatCast}(1) = 1$$$
Lean4
/-- Internal: Not intended to be used outside this local construction. -/
@[simp]
theorem pnatCast_one [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ((1 : ℕ+) : Rˣ) = 1 :=
by
apply Units.ext
rw [Units.val_one]
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1
rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]
rw [PNat.one_coe, Nat.cast_one]