{"id":991,"date":"2022-09-02T06:00:03","date_gmt":"2022-09-02T04:00:03","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=991"},"modified":"2022-09-11T13:57:43","modified_gmt":"2022-09-11T11:57:43","slug":"si-r-es-un-anillo-y-a-%e2%88%88-r-entonces-a-0-0","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-r-es-un-anillo-y-a-%e2%88%88-r-entonces-a-0-0\/","title":{"rendered":"Si R es un anillo y a \u2208 R, entonces a * 0 = 0"},"content":{"rendered":"

Demostrar que Si R es un anillo y a \u2208 R, entonces<\/p>\n

\na * 0 = 0\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariable  a : R\n\nexample : a * 0 = 0 :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariable  a : R\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : (mul_add a 0 0).symm\n     ... = a * 0       : congr_arg (\u03bb x, a * x) (add_zero 0)\n     ... = a * 0 + 0   : (add_zero (a * 0)).symm,\n  rw add_left_cancel h\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : by rw \u2190mul_add\n     ... = a * 0       : by rw add_zero\n     ... = a * 0 + 0   : by rw add_zero,\n  rw add_left_cancel h\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n  { rw [\u2190mul_add, add_zero, add_zero] },\n  rw add_left_cancel h\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : by simp\n     ... = a * 0       : by simp\n     ... = a * 0 + 0   : by simp,\n  simp,\nend\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nby simp\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\n-- by library_search\nmul_zero a\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n