English
If k ≠ 0, then Fermat42 a b c is equivalent to Fermat42 (k a) (k b) (k^2 c).
Русский
Если k не равно нулю, то Fermat42 a b c эквивалентна Fermat42 (k a) (k b) (k^2 c).
LaTeX
$$$k \\neq 0 \\rightarrow (Fermat42\\ a\\ b\\ c \\iff Fermat42\\ (k a)\\ (k b)\\ (k^2 c))$$$
Lean4
theorem mul {a b c k : ℤ} (hk0 : k ≠ 0) : Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c) :=
by
delta Fermat42
constructor
· intro f42
constructor
· exact mul_ne_zero hk0 f42.1
constructor
· exact mul_ne_zero hk0 f42.2.1
· have H : a ^ 4 + b ^ 4 = c ^ 2 := f42.2.2
linear_combination k ^ 4 * H
· intro f42
constructor
· exact right_ne_zero_of_mul f42.1
constructor
· exact right_ne_zero_of_mul f42.2.1
apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp
linear_combination f42.2.2
