Demostrar con Lean4 que si \\(m, n \\in \\mathbb{N}\\) son n\u00fameros naturales, entonces
\n\\[\\gcd(m, n) = \\gcd(n, m)\\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nvariable (k m n : \u2115)\r\n\r\nopen Nat\r\n\r\nexample : gcd m n = gcd n m :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nEs consecuencia del siguiente lema auxiliar
\n\\[ (\\forall x, y \\in \\mathbb{N})[\\gcd(x,y) \\mid \\gcd(y,x)] \\tag{1} \\]
\nEn efecto, sustituyendo en (1) \\(x\\) por \\(m\\) e \\(y\\) por \\(n\\), se tiene
\n\\[ \\gcd(m, n) \\mid \\gcd(n, m) \\tag{2}\\]
\ny, sustituyendo en (1) \\(x\\) por \\(n\\) e \\(y\\) por \\(m\\), se tiene
\n\\[ \\gcd(n, m) \\mid \\gcd(m, n) \\tag{3} \\]
\nFinalmente, aplicando la propiedad antisim\u00e9trica de la divisibilidad a (2) y (3), se tiene
\n\\[ \\gcd(m, n) = \\gcd(n, m) \\]<\/p>\n
Para demostrar (1), por la definici\u00f3n del m\u00e1ximo com\u00fan divisor, basta demostrar las siguientes relaciones
\n\\begin{align}
\n \\gcd(m, n) &\\mid n \\\\
\n \\gcd(m, n) &\\mid m
\n\\end{align}
\ny ambas se tienen por la definici\u00f3n del m\u00e1ximo com\u00fan divisor.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nvariable (k m n : \u2115)\r\n\r\nopen Nat\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\r\nlemma aux : gcd m n \u2223 gcd n m :=\r\nby\r\n have h1 : gcd m n \u2223 n :=\r\n gcd_dvd_right m n\r\n have h2 : gcd m n \u2223 m :=\r\n gcd_dvd_left m n\r\n show gcd m n \u2223 gcd n m\r\n exact dvd_gcd h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\r\nexample : gcd m n \u2223 gcd n m :=\r\ndvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : gcd m n = gcd n m :=\r\nby\r\n have h1 : gcd m n \u2223 gcd n m := aux m n\r\n have h2 : gcd n m \u2223 gcd m n := aux n m\r\n show gcd m n = gcd n m\r\n exact _root_.dvd_antisymm h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : gcd m n = gcd n m :=\r\nby\r\n apply _root_.dvd_antisymm\r\n { exact aux m n }\r\n { exact aux n m }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : gcd m n = gcd n m :=\r\n_root_.dvd_antisymm (aux m n) (aux n m)\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : gcd m n = gcd n m :=\r\n-- by apply?\r\ngcd_comm m n\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (_root_.dvd_antisymm : m \u2223 n \u2192 n \u2223 m \u2192 m = n)\r\n-- #check (dvd_gcd : k \u2223 m \u2192 k \u2223 n \u2192 k \u2223 gcd m n)\r\n-- #check (gcd_comm m n : gcd m n = gcd n m)\r\n-- #check (gcd_dvd_left m n: gcd m n \u2223 m)\r\n-- #check (gcd_dvd_right m n : gcd m n \u2223 n)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n