add_self
theorem add_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), a + a = 0
This theorem states that for any type `α` which forms a Boolean ring, the sum of any element `a` from `α` with itself (i.e., `a + a`) equals zero. In mathematical terms, for all `a` in a Boolean ring, `a + a = 0`.
More concisely: In a Boolean ring, the sum of any element with itself equals zero. (i.e., for all `a` in a Boolean ring, `a + a = 0`)
|
BooleanRing.mul_self
theorem BooleanRing.mul_self : ∀ {α : Type u_4} [self : BooleanRing α] (a : α), a * a = a
This theorem states that in any Boolean ring, the multiplication of any element with itself always yields the original element. In more mathematical terms, for any Boolean ring `α` and any element `a` of `α`, `a * a = a`. This property is known as idempotence in multiplication.
More concisely: In any Boolean ring, the multiplication of an element by itself equals the element itself. (idempotent multiplication)
|
mul_self
theorem mul_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), a * a = a
This theorem, named `mul_self`, states that for all elements `a` of a given type `α`, where `α` is a Boolean Ring, the product of `a` with itself (i.e., `a * a`) is equal to `a` itself. In mathematical terms, for any element `a` in a Boolean Ring, `a² = a`.
More concisely: In a Boolean Ring, for all elements `a`, `a * a = a`.
|