Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-14 14:51 9daf78bc

View on Github →

feat(tactic/linarith): basic support for nat (#343)

feat(tactic/linarith): basic support for nats
fix(tactic/linarith): typo

Estimated changes

Modified tactic/linarith.lean

added theorem linarith.int.coe_nat_bit0

added theorem linarith.int.coe_nat_bit1

added theorem linarith.nat_eq_subst

added theorem linarith.nat_le_subst

added theorem linarith.nat_lt_subst

Modified tests/linarith.lean