Theorem Denumerable.ofNat_of_decode

Modification history

2025-06-02 07:15

Mathlib/Logic/Denumerable.lean

chore: improve simp-set by putting hypotheses in simp normal form (#25024)

Modified Denumerable.ofNat_of_decode View on Github →

2023-01-20 07:09

Mathlib/Logic/Denumerable.lean

feat: port Logic.Denumerable (#1682)

Added Denumerable.ofNat_of_decode View on Github →