Commit 2024-06-08 14:38 80dbecb2

View on Github →

feat: topology on ℕ+(PNat) (#13250)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/PNat.lean

added theorem PNat.dist_coe

added theorem PNat.dist_eq

added theorem PNat.uniformEmbedding_coe