pnatCast_one — Mathlib

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]

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