Si m, n ∈ ℕ, entonces gcd(m,n) = gcd(n,m)
Demostrar que si m, n ∈ ℕ, entonces gcd(m,n) = gcd(n,m).
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.nat.gcd open nat variables k m n : ℕ example : gcd m n = gcd n m := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 |
import data.nat.gcd open nat variables k m n : ℕ -- 1ª demostración -- =============== example : gcd m n = gcd n m := begin have h1 : gcd m n ∣ gcd n m, { have h1a : gcd m n ∣ n, by exact gcd_dvd_right m n, have h1b : gcd m n ∣ m, by exact gcd_dvd_left m n, show gcd m n ∣ gcd n m, by exact dvd_gcd h1a h1b, }, have h2 : gcd n m ∣ gcd m n, { have h2a : gcd n m ∣ m, by exact gcd_dvd_right n m, have h2b : gcd n m ∣ n, by exact gcd_dvd_left n m, show gcd n m ∣ gcd m n, by exact dvd_gcd h2a h2b, }, show gcd m n = gcd n m, by exact dvd_antisymm h1 h2, end -- 2ª demostración -- =============== example : gcd m n = gcd n m := begin apply dvd_antisymm, { apply dvd_gcd, { exact gcd_dvd_right m n, }, { exact gcd_dvd_left m n, }}, { apply dvd_gcd, { exact gcd_dvd_right n m, }, { exact gcd_dvd_left n m, }}, end -- 3ª demostración -- =============== example : gcd m n = gcd n m := begin apply dvd_antisymm, { apply dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)}, { apply dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m)}, end -- 4ª demostración -- =============== example : gcd m n = gcd n m := dvd_antisymm (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)) (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m)) -- 5ª demostración -- =============== lemma aux : gcd m n ∣ gcd n m := begin have h1 : gcd m n ∣ n, by exact gcd_dvd_right m n, have h2 : gcd m n ∣ m, by exact gcd_dvd_left m n, show gcd m n ∣ gcd n m, by exact dvd_gcd h1 h2, end example : gcd m n = gcd n m := begin apply dvd_antisymm, { exact aux m n, }, { exact aux n m, }, end -- 6ª demostración -- =============== lemma aux2 : gcd m n ∣ gcd n m := dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n) example : gcd m n = gcd n m := dvd_antisymm (aux2 m n) (aux2 n m) -- 7ª demostración -- =============== example : gcd m n = gcd n m := -- by library_search gcd_comm m n |
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. 21.
