Si x ∈ ℕ, entonces x ∣ x²
Demostrar que si x ∈ ℕ, entonces
|
1 |
x ∣ x^2 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.nat.pow variable x : ℕ example : x ∣ x^2 := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import data.nat.pow variable x : ℕ -- 1ª demostración -- =============== example : x ∣ x^2 := begin rw pow_two, apply dvd_mul_right, end -- 2ª demostración -- =============== example : x ∣ x^2 := by apply dvd_mul_right |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 20.
