32 lines
1.4 KiB
Lean4
32 lines
1.4 KiB
Lean4
import Game.Levels.AdvMultiplication.L01mul_le_mul_right
|
|
import Game.Levels.AdvMultiplication.L02mul_left_ne_zero
|
|
import Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
|
|
import Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
|
|
import Game.Levels.AdvMultiplication.L05le_mul_right
|
|
import Game.Levels.AdvMultiplication.L06mul_right_eq_one
|
|
import Game.Levels.AdvMultiplication.L07mul_ne_zero
|
|
import Game.Levels.AdvMultiplication.L08mul_eq_zero
|
|
import Game.Levels.AdvMultiplication.L09mul_left_cancel
|
|
import Game.Levels.AdvMultiplication.L10mul_right_eq_self
|
|
|
|
World "AdvMultiplication"
|
|
Title "Advanced Multiplication World"
|
|
|
|
Introduction
|
|
"
|
|
Advanced *Addition* World proved various implications
|
|
involving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.
|
|
These lemmas were used to prove basic facts about ≤ in ≤ World.
|
|
|
|
In Advanced Multiplication World we prove analogous
|
|
facts about multiplication, such as `x * y = 1 → x = 1`, and
|
|
`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare
|
|
us for Divisibility World.
|
|
|
|
Multiplication World is more complex than Addition World. In the same
|
|
way, Advanced Multiplication world is more complex than Advanced Addition
|
|
World. One reason for this is that certain intermediate results are only
|
|
true under the additional hypothesis that one of the variables is non-zero.
|
|
This causes some unexpected extra twists.
|
|
"
|