half_add_self
theorem half_add_self : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), (a + a) / 2 = a := by
sorry
This theorem, `half_add_self`, states that for any type `R` that is a division ring with characteristic zero, the half of the sum of any element `a` with itself equals `a`. In other words, it asserts that for any element `a` in a division ring `R` with characteristic zero, the equation $(a + a) / 2 = a$ holds.
More concisely: For any element `a` in a division ring `R` with characteristic zero, (`a + a`) / 2 = `a`.
|
add_self_eq_zero
theorem add_self_eq_zero :
∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
a + a = 0 ↔ a = 0
This theorem states that for any type `R` that is a non-associative semiring, with no zero divisors and of characteristic zero, an element `a` of `R` will satisfy the equation `a + a = 0` if and only if `a` is zero. In other words, within such a structure, the only element that, when added to itself, results in zero is the zero element itself.
More concisely: In a non-associative semiring of characteristic zero with no zero divisors, an element is zero if and only if it satisfies the equation `a + a = 0`.
|
add_halves'
theorem add_halves' : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a / 2 + a / 2 = a := by
sorry
This theorem states that for any division ring `R` that has characteristic zero, for any element `a` of `R`, the sum of `a` divided by 2 and `a` divided by 2 equals `a`. In simpler terms, it means that in any division ring with characteristic zero, adding half of a number to itself would yield the original number. The characteristic of a ring is zero if and only if the ring's additive identity (zero) is not reached by repeatedly adding the ring's multiplicative identity (one) to itself.
More concisely: In any division ring of characteristic zero, the element `a` satisfies `(a : R) / 2 + (a : R) / 2 = a`.
|
eq_neg_self_iff
theorem eq_neg_self_iff :
∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] [inst_2 : CharZero R] {a : R},
a = -a ↔ a = 0
This theorem states that for any element `a` of a type `R`, where `R` is a non-associative ring with no zero divisors and zero character, `a` equals its own negation if and only if `a` is zero. In other words, the only element in such a ring that is equal to its own negative is the zero element.
More concisely: In a non-associative ring without zero divisors and zero character, an element equals its own negation if and only if it is the additive identity (zero).
|
sub_half
theorem sub_half : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] (a : R), a - a / 2 = a / 2
This theorem states that for any element `a` of any Division Ring `R` (which is not of characteristic zero), the result of subtracting half of `a` from `a` is equal to half of `a`. In other words, for all `a` in `R`, `a - a / 2 = a / 2`.
More concisely: For any element `a` in a non-zero characteristic Division Ring `R`, `a - a / 2 = a / 2`.
|