LeanAide GPT-4 documentation

Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone



CochainComplex.mappingCone.desc.proof_1

theorem CochainComplex.mappingCone.desc.proof_1 : -1 + 1 = 0

This theorem, named `CochainComplex.mappingCone.desc.proof_1`, establishes a basic property of integer arithmetic, specifically that the sum of `-1` and `1` equals `0`. It's a simple yet fundamental theorem that shows the additive inverse property where adding a number and its negative counterpart results in zero.

More concisely: The theorem asserts that for all integers x, -x + x = 0.