Theorems · Theorem · commutative algebra

Nat.unaryCast.eq_def

∀ {R : Type u_1} [inst : One R] [inst_1 : Zero R] [inst_2 : Add R] (x : ℕ),
  x.unaryCast =
    match x with
    | 0 => 0
    | n.succ => n.unaryCast + 1

Defined in: Mathlib.RingTheory.FractionalIdeal.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: One Zero Add

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nat.unaryCaststatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.