{"id":984,"date":"2022-08-30T16:00:29","date_gmt":"2022-08-30T14:00:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=984"},"modified":"2022-09-11T13:58:52","modified_gmt":"2022-09-11T11:58:52","slug":"si-r-es-un-anillo-y-a-b-%e2%88%88-r-entonces-a-b-b-a","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-b-b-a\/","title":{"rendered":"Si R es un anillo y a, b \u2208 R, entonces (a + b) + -b = a"},"content":{"rendered":"

Demostrar que si R es un anillo, entonces<\/p>\n

\n   \u2200 a b : R, (a + b) + -b = a\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\nexample : (a + b) + -b = a :=\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\n-- ===============\n\nexample : (a + b) + -b = a :=\ncalc (a + b) + -b\n     = a + (b + -b) : by rw add_assoc\n ... = a + 0        : by rw add_right_neg\n ... = a            : by rw add_zero\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\nbegin\n  rw add_assoc,\n  rw add_right_neg,\n  rw add_zero,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\nby rw [add_assoc, add_right_neg, add_zero]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\n-- by library_search\nadd_neg_eq_of_eq_add rfl\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\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