Commit 2022-12-16 13:20 8d5a5528

View on Github →

feat port: Data.Nat.Dist (#1023) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Dist.lean

added theorem Nat.dist.def

added theorem Nat.dist.triangle_inequality

added def Nat.dist

added theorem Nat.dist_add_add_left

added theorem Nat.dist_add_add_right

added theorem Nat.dist_comm

added theorem Nat.dist_eq_intro

added theorem Nat.dist_eq_sub_of_le

added theorem Nat.dist_eq_sub_of_le_right

added theorem Nat.dist_eq_zero

added theorem Nat.dist_mul_left

added theorem Nat.dist_mul_right

added theorem Nat.dist_pos_of_ne

added theorem Nat.dist_self

added theorem Nat.dist_succ_succ

added theorem Nat.dist_tri_left'

added theorem Nat.dist_tri_left

added theorem Nat.dist_tri_right'

added theorem Nat.dist_tri_right

added theorem Nat.dist_zero_left

added theorem Nat.dist_zero_right

added theorem Nat.eq_of_dist_eq_zero