Zulip Chat Archive

Stream: general

Topic: no mul_sub in int?

onriv (Jan 21 2023 at 08:25):

Hi. I am following the tutorial https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html but found the following example failed:

import data.int.basic

variables a b c d : 
example : a * (b - c) = a * b - a * c := mul_sub a b c

for no mul_sub any more. Any way to define it again? Thanks!

onriv (Jan 21 2023 at 09:50):

Ah my bad, in fact there are mul_sub and sub_mul in init.data.int.basic

Last updated: Aug 03 2023 at 10:10 UTC