CochainComplex.shiftFunctorAdd'.proof_1
theorem CochainComplex.shiftFunctorAdd'.proof_1 : ∀ (n₁ n₂ n₁₂ : ℤ), n₁ + n₂ = n₁₂ → ∀ (i : ℤ), i + n₂ + n₁ = i + n₁₂
This theorem states that for any integers `n₁`, `n₂`, and `n₁₂` such that `n₁ + n₂ = n₁₂`, and for any integer `i`, the equality `i + n₂ + n₁ = i + n₁₂` holds. In other words, if `n₁₂` is the sum of `n₁` and `n₂`, then adding `n₁` and `n₂` in any order to `i` gives the same result as adding `n₁₂` to `i`.
More concisely: For any integers `n₁`, `n₂`, and `i`, if `n₁ + n₂ = n₁₂`, then `i + n₁ + n₂ = i + n₁₂`.
|
CochainComplex.shiftFunctorObjXIso.proof_1
theorem CochainComplex.shiftFunctorObjXIso.proof_1 : ∀ (n i m : ℤ), m = i + n → i + n = m
This theorem states that for any three integers `n`, `i`, and `m`, if `m` is equal to the sum of `i` and `n`, then the sum of `i` and `n` is also equal to `m`. It is essentially confirming the symmetric property of equality in the context of integer arithmetic.
More concisely: If `m` equals the sum of `i` and `n`, then `i` plus `n` equals `m`.
|