{"id":980,"date":"2022-08-29T16:00:01","date_gmt":"2022-08-29T14:00:01","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=980"},"modified":"2022-09-11T13:44:42","modified_gmt":"2022-09-11T11:44:42","slug":"si-r-es-un-anillo-y-a-b-%e2%88%88-r-entonces-a-a-b-b","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-r-es-un-anillo-y-a-b-%e2%88%88-r-entonces-a-a-b-b\/","title":{"rendered":"Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b"},"content":{"rendered":"

En Lean, se declara que R es un anillo mediante la expresi\u00f3n<\/p>\n

\n   variables {R : Type*} [ring R]\n<\/pre>\n
y, como consecuencia, se tienen los siguientes axiomas<\/p>\n
\n   add_assoc    : \u2200 a b c : R, (a + b) + c = a + (b + c)\n   add_comm     : \u2200 a b : R,   a + b = b + a\n   zero_add     : \u2200 a : R,     0 + a = a\n   add_left_neg : \u2200 a : R,     -a + a = 0\n   mul_assoc    : \u2200 a b c : R, a * b * c = a * (b * c)\n   mul_one      : \u2200 a : R,     a * 1 = a\n   one_mul      : \u2200 a : R,     1 * a = a\n   mul_add      : \u2200 a b c : R, a * (b + c) = a * b + a * c\n   add_mul      : \u2200 a b c : R, (a + b) * c = a * c + b * c\n<\/pre>\n
Demostrar que si R es un anillo, entonces<\/p>\n
\n   \u2200 a b : R, -a + (a + b) = b\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\nexample\n  : -a + (a + b) = b :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\ncalc -a + (a + b)\n     = (-a + a) + b : by rw \u2190 add_assoc\n ... = 0 + b        : by rw add_left_neg\n ... = b            : by rw zero_add\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\nbegin\n  rw \u2190add_assoc,\n  rw add_left_neg,\n  rw zero_add,\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\nby rw [\u2190add_assoc, add_left_neg, zero_add]\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\n-- by library_search\nneg_add_cancel_left a b\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\n-- by hint\nby finish\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n