{"id":8018,"date":"2023-09-16T13:23:22","date_gmt":"2023-09-16T11:23:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8018"},"modified":"2023-09-16T13:23:22","modified_gmt":"2023-09-16T11:23:22","slug":"16-sep-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/16-sep-23\/","title":{"rendered":"La semana en Calculemus (16 de septiembre de 2023)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. En \u211d, |a| &#8211; |b| \u2264 |a &#8211; b|<\/a><\/li>\n<li><a href=\"#ej2\">2. Si x, y, z \u2208 \u2115, entonces x divide a yxz<\/a><\/li>\n<li><a href=\"#ej3\">3. Si x divide a w, entonces tambi\u00e9n divide a y(xz)+x\u00b2+w\u00b2<\/a><\/li>\n<li><a href=\"#ej4\">4. Conmutatividad del m\u00e1ximo com\u00fan divisor<\/a><\/li>\n<li><a href=\"#ej5\">5. En los ret\u00edculos, x \u2293 y = y \u2293 x<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. En \u211d, |a| &#8211; |b| \u2264 |a &#8211; b|<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) y &#92;(b&#92;) n\u00fameros reales, entonces<br \/>\n&#92;[|a| &#8211; |b| &#92;leq |a &#8211; b|&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\nexample : |a| - |b| \u2264 |a - b| :=\nby sorry\n<\/pre>\n<p><b>Demostraciones en lenguaje natural (LN)<\/b><\/p>\n<p><b>1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Por la siguiente cadena de desigualdades<br \/>\n&#92;begin{align}<br \/>\n   |a| &#8211; |b| &amp;= |a &#8211; b + b| &#8211; |b| &#92;&#92;<br \/>\n             &amp;&#92;leq (|a &#8211; b| + |b|) &#8211; |b|   &amp;&amp;&#92;text{[por la desigualdad triangular]}&#92;&#92;<br \/>\n             &amp;= |a &#8211; b|<br \/>\n&#92;end{align}<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Por la desigualdad triangular<br \/>\n&#92;[   |a &#8211; b + b| &#92;leq |a &#8211; b| + |b| &#92;]<br \/>\nsimplificando en la izquierda<br \/>\n&#92;[   |a| &#92;leq |a &#8211; b| + |b| &#92;]<br \/>\ny, pasando &#92;(|b|&#92;) a la izquierda<br \/>\n&#92;[   |a| &#8211; |b| \u2264 |a &#8211; b| &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\nexample : |a| - |b| \u2264 |a - b| :=\ncalc |a| - |b|\n     = |a - b + b| - |b| :=\n          congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm\n   _ \u2264 (|a - b| + |b|) - |b| :=\n           sub_le_sub_right (abs_add (a - b) b) (|b|)\n   _ = |a - b| :=\n          add_sub_cancel (|a - b|) (|b|)\n\n-- 2\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\nexample : |a| - |b| \u2264 |a - b| :=\ncalc |a| - |b|\n     = |a - b + b| - |b| := by\n          rw [sub_add_cancel]\n   _ \u2264 (|a - b| + |b|) - |b| := by\n          apply sub_le_sub_right\n          apply abs_add\n   _ = |a - b| := by\n          rw [add_sub_cancel]\n\n-- 3\u00aa demostraci\u00f3n (basada en la 2\u00aa en LN)\nexample : |a| - |b| \u2264 |a - b| :=\nby\n  have h1 : |a - b + b| \u2264 |a - b| + |b| := abs_add (a - b) b\n  rw [sub_add_cancel] at h1\n  exact abs_sub_abs_le_abs_sub a b\n\n-- 4\u00aa demostraci\u00f3n\nexample : |a| - |b| \u2264 |a - b| :=\nabs_sub_abs_le_abs_sub a b\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/abs_sub.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 18.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si x, y, z \u2208 \u2115, entonces x divide a yxz<\/h3>\n<p>Demostrar con Lean4 que si &#92;(x,y,z &#92;in &#92;mathbb{N}&#92;), entonces &#92;(x &#92;mid yxz&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y z : \u2115)\n\nexample : x \u2223 y * x * z :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la transitividad de la divisibilidad aplicada a las relaciones<br \/>\n&#92;begin{align}<br \/>\n    x &amp;&#92;mid yx &#92;&#92;<br \/>\n   yx &amp;&#92;mid yxz<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y z : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\nby\n  have h1 : x \u2223 y * x :=\n    dvd_mul_left x y\n  have h2 : (y * x) \u2223 (y * x * z) :=\n    dvd_mul_right (y * x) z\n  show x \u2223 y * x * z\n  exact dvd_trans h1 h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\ndvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\nby\n  apply dvd_mul_of_dvd_left\n  apply dvd_mul_left\n\n\n-- Los lemas utilizados son:\n#check (dvd_mul_left x y : x \u2223 y * x)\n#check (dvd_mul_right x y : x \u2223 x * y)\n#check (dvd_trans : x \u2223 y \u2192 y \u2223 z \u2192 x \u2223 z)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Divisibilidad_de_producto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 19.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si x divide a w, entonces tambi\u00e9n divide a y(xz)+x\u00b2+w\u00b2<\/h3>\n<p>Demostrar con Lean4 que si &#92;(x&#92;) divide a &#92;(w&#92;), entonces tambi\u00e9n divide a &#92;(y(xz)+x^2+w^2&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (w x y z : \u2115)\n\nexample\n  (h : x \u2223 w)\n  : x \u2223 y * (x * z) + x^2 + w^2 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la divisibilidad de la suma basta probar que<br \/>\n&#92;begin{align}<br \/>\n   x &amp;&#92;mid yxz &#92;tag{1} &#92;&#92;<br \/>\n   x &amp;&#92;mid x^2 &#92;tag{2} &#92;&#92;<br \/>\n   x &amp;&#92;mid w^2 &#92;tag{3}<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar (1), por la divisibilidad del producto se tiene<br \/>\n&#92;[   x &#92;mid xz&#92;]<br \/>\ny, de nuevo por la divisibilidad del producto,<br \/>\n&#92;[   x &#92;mid y(xz)&#92;]<\/p>\n<p>La propiedad (2) se tiene por la definici\u00f3n de cuadrado y la divisibilidad del producto.<\/p>\n<p>La propiedad (3) se tiene por la definici\u00f3n de cuadrado, la hip\u00f3tesis y la divisibilidad del producto.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (w x y z : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : x \u2223 w)\n  : x \u2223 y * (x * z) + x^2 + w^2 :=\nby\n  have h1 : x \u2223 x * z :=\n    dvd_mul_right x z\n  have h2 : x \u2223 y * (x * z) :=\n    dvd_mul_of_dvd_right h1 y\n  have h3 : x \u2223 x^2 := by\n    apply dvd_mul_left\n  have h4 : x \u2223 w * w :=\n    dvd_mul_of_dvd_left h w\n  have h5 : x \u2223 w^2 := by\n    rwa [\u2190 pow_two w] at h4\n  have h6 : x \u2223 y * (x * z) + x^2 :=\n    dvd_add h2 h3\n  show x \u2223 y * (x * z) + x^2 + w^2\n  exact dvd_add h6 h5\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : x \u2223 w)\n  : x \u2223 y * (x * z) + x^2 + w^2 :=\nby\n  apply dvd_add\n  { apply dvd_add\n    { apply dvd_mul_of_dvd_right\n      apply dvd_mul_right }\n    { rw [pow_two]\n      apply dvd_mul_right }}\n  { rw [pow_two]\n    apply dvd_mul_of_dvd_left h }\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : x \u2223 w)\n  : x \u2223 y * (x * z) + x^2 + w^2 :=\nby\n  repeat' apply dvd_add\n  { apply dvd_mul_of_dvd_right\n    apply dvd_mul_right }\n  { rw [pow_two]\n    apply dvd_mul_right }\n  { rw [pow_two]\n    apply dvd_mul_of_dvd_left h }\n\n-- Lemas usados\n-- ============\n\n-- #check (dvd_add : x \u2223 y \u2192 x \u2223 z \u2192 x \u2223 y + z)\n-- #check (dvd_mul_left x y : x \u2223 y * x)\n-- #check (dvd_mul_right x y : x \u2223 x * y)\n-- #check (dvd_mul_of_dvd_left : x \u2223 y \u2192 \u2200 (c : \u2115), x \u2223 y * c)\n-- #check (dvd_mul_of_dvd_right : x \u2223 y \u2192 \u2200 (c : \u2115), x \u2223 c * y)\n-- #check (pow_two x : x ^ 2 = x * x)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Ejercicio_de_divisibilidad.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 19.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Conmutatividad del m\u00e1ximo com\u00fan divisor<\/h3>\n<p>Demostrar con Lean4 que si &#92;(m, n &#92;in &#92;mathbb{N}&#92;) son n\u00fameros naturales, entonces<br \/>\n&#92;[&#92;gcd(m, n) = &#92;gcd(n, m)&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (k m n : \u2115)\n\nopen Nat\n\nexample : gcd m n = gcd n m :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Es consecuencia del siguiente lema auxiliar<br \/>\n&#92;[   (&#92;forall x, y &#92;in &#92;mathbb{N})[&#92;gcd(x,y) &#92;mid &#92;gcd(y,x)] &#92;tag{1} &#92;]<br \/>\nEn efecto, sustituyendo en (1) &#92;(x&#92;) por &#92;(m&#92;) e &#92;(y&#92;) por &#92;(n&#92;), se tiene<br \/>\n&#92;[   &#92;gcd(m, n) &#92;mid &#92;gcd(n, m) &#92;tag{2}&#92;]<br \/>\ny, sustituyendo en (1) &#92;(x&#92;) por &#92;(n&#92;) e &#92;(y&#92;) por &#92;(m&#92;), se tiene<br \/>\n&#92;[   &#92;gcd(n, m) &#92;mid &#92;gcd(m, n) &#92;tag{3} &#92;]<br \/>\nFinalmente, aplicando la propiedad antisim\u00e9trica de la divisibilidad a (2) y (3), se tiene<br \/>\n&#92;[   &#92;gcd(m, n) = &#92;gcd(n, m) &#92;]<\/p>\n<p>Para demostrar (1), por la definici\u00f3n del m\u00e1ximo com\u00fan divisor, basta demostrar las siguientes relaciones<br \/>\n&#92;begin{align}<br \/>\n   &#92;gcd(m, n) &amp;&#92;mid n &#92;&#92;<br \/>\n   &#92;gcd(m, n) &amp;&#92;mid m<br \/>\n&#92;end{align}<br \/>\ny ambas se tienen por la definici\u00f3n del m\u00e1ximo com\u00fan divisor.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (k m n : \u2115)\n\nopen Nat\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\nlemma aux : gcd m n \u2223 gcd n m :=\nby\n  have h1 : gcd m n \u2223 n :=\n    gcd_dvd_right m n\n  have h2 : gcd m n \u2223 m :=\n    gcd_dvd_left m n\n  show gcd m n \u2223 gcd n m\n  exact dvd_gcd h1 h2\n\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\nexample : gcd m n \u2223 gcd n m :=\ndvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)\n\n-- 1\u00aa demostraci\u00f3n\nexample : gcd m n = gcd n m :=\nby\n  have h1 : gcd m n \u2223 gcd n m := aux m n\n  have h2 : gcd n m \u2223 gcd m n := aux n m\n  show gcd m n = gcd n m\n  exact _root_.dvd_antisymm h1 h2\n\n-- 2\u00aa demostraci\u00f3n\nexample : gcd m n = gcd n m :=\nby\n  apply _root_.dvd_antisymm\n  { exact aux m n }\n  { exact aux n m }\n\n-- 3\u00aa demostraci\u00f3n\nexample : gcd m n = gcd n m :=\n_root_.dvd_antisymm (aux m n) (aux n m)\n\n-- 4\u00aa demostraci\u00f3n\nexample : gcd m n = gcd n m :=\n-- by apply?\ngcd_comm m n\n\n-- Lemas usados\n-- ============\n\n-- #check (_root_.dvd_antisymm : m \u2223 n \u2192 n \u2223 m \u2192 m = n)\n-- #check (dvd_gcd : k \u2223 m \u2192 k \u2223 n \u2192 k \u2223 gcd m n)\n-- #check (gcd_comm m n : gcd m n = gcd n m)\n-- #check (gcd_dvd_left  m n: gcd m n \u2223 m)\n-- #check (gcd_dvd_right m n : gcd m n \u2223 n)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Conmutatividad_del_gcd.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 19.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En los ret\u00edculos, x \u2293 y = y \u2293 x<\/h3>\n<p>Demostrar con Lean4 que en los ret\u00edculos se verifica que<br \/>\n&#92;[x \u2293 y = y \u2293 x&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Order.Lattice\nvariable {\u03b1 : Type _} [Lattice \u03b1]\nvariable (x y z : \u03b1)\n\nexample : x \u2293 y = y \u2293 x :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Es consecuencia del siguiente lema auxiliar<br \/>\n&#92;[   (\u2200 a, b)[a \u2293 b \u2264 b \u2293 a] &#92;tag{1} &#92;]<br \/>\nEn efecto, sustituyendo en (1) &#92;(a&#92;) por &#92;(x&#92;) y &#92;(b&#92;) por &#92;(y&#92;), se tiene<br \/>\n&#92;[   x \u2293 y \u2264 y \u2293 x &#92;tag{2} &#92;]<br \/>\ny sustituyendo en (1) &#92;(a&#92;) por &#92;(y&#92;) y &#92;(b&#92;) por &#92;(x&#92;), se tiene<br \/>\n&#92;[   y \u2293 x \u2264 x \u2293 y &#92;tag{3} &#92;]<br \/>\nFinalmente, aplicando la propiedad antisim\u00e9trica de la divisibilidad a (2) y (3), se tiene<br \/>\n&#92;[   x \u2293 y = y \u2293 x &#92;]<\/p>\n<p>Para demostrar (1), por la definici\u00f3n del \u00ednfimo, basta demostrar las siguientes relaciones<br \/>\n&#92;begin{align}<br \/>\n   y \u2293 x &amp;\u2264 x &#92;&#92;<br \/>\n   y \u2293 x &amp;\u2264 y<br \/>\n&#92;end{align}<br \/>\ny ambas se tienen por la definici\u00f3n del \u00ednfimo.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Order.Lattice\nvariable {\u03b1 : Type _} [Lattice \u03b1]\nvariable (x y z : \u03b1)\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\nlemma aux : x \u2293 y \u2264 y \u2293 x :=\nby\n  have h1 : x \u2293 y \u2264 y :=\n    inf_le_right\n  have h2 : x \u2293 y \u2264 x :=\n    inf_le_left\n  show x \u2293 y \u2264 y \u2293 x\n  exact le_inf h1 h2\n\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\nexample : x \u2293 y \u2264 y \u2293 x :=\nby\n  apply le_inf\n  { apply inf_le_right }\n  { apply inf_le_left }\n\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\nexample : x \u2293 y \u2264 y \u2293 x :=\nle_inf inf_le_right inf_le_left\n\n-- 1\u00aa demostraci\u00f3n\nexample : x \u2293 y = y \u2293 x :=\nby\n  have h1 : x \u2293 y \u2264 y \u2293 x :=\n    aux x y\n  have h2 : y \u2293 x \u2264 x \u2293 y :=\n    aux y x\n  show x \u2293 y = y \u2293 x\n  exact le_antisymm h1 h2\n\n-- 2\u00aa demostraci\u00f3n\nexample : x \u2293 y = y \u2293 x :=\nby\n  apply le_antisymm\n  { apply aux }\n  { apply aux }\n\n-- 3\u00aa demostraci\u00f3n\nexample : x \u2293 y = y \u2293 x :=\nle_antisymm (aux x y) (aux y x)\n\n-- 4\u00aa demostraci\u00f3n\nexample : x \u2293 y = y \u2293 x :=\nby apply le_antisymm; simp ; simp\n\n-- 5\u00aa demostraci\u00f3n\nexample : x \u2293 y = y \u2293 x :=\n-- by apply?\ninf_comm\n\n-- Lemas usados\n-- ============\n\n-- #check (inf_comm : x \u2293 y = y \u2293 x)\n-- #check (inf_le_left : x \u2293 y \u2264 x)\n-- #check (inf_le_right : x \u2293 y \u2264 y)\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\n-- #check (le_inf : z \u2264 x \u2192 z \u2264 y \u2192 z \u2264 x \u2293 y)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Conmutatividad_del_infimo.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 20.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. En \u211d, |a| &#8211; |b| \u2264 |a &#8211; b| 2. Si x, y, z \u2208 \u2115, entonces x divide a yxz 3. Si x divide a w, entonces tambi\u00e9n divide a y(xz)+x\u00b2+w\u00b2 4. Conmutatividad del m\u00e1ximo com\u00fan divisor 5. En&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8018"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8018"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8018\/revisions"}],"predecessor-version":[{"id":8019,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8018\/revisions\/8019"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8018"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8018"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8018"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}