ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
292 stars 73 forks source link

Improve wording in multiplication distributivity lemmas #120

Closed chezbgone closed 2 years ago

chezbgone commented 2 years ago

"Addition is distributive over multiplication." means that a + (b * c) = (a + b) * (a + c), which is not true in general. Usually I hear "left distributive" to mean multiplication on the left, and "right distributive" to mean multiplication on the right, so that's what I have changed it to here.