Commit 2020-07-19 15:29 9b0435a0
View on Github →fix(tactic/linarith): find correct zero_lt_one (#3455) Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/linarith.20and.20ordinal.20file
fix(tactic/linarith): find correct zero_lt_one (#3455) Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/linarith.20and.20ordinal.20file