CharTwo.neg_eq
theorem CharTwo.neg_eq : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : CharP R 2] (x : R), -x = x
This theorem states that for any ring `R` of characteristic 2, the negation of any element `x` in `R` is equal to `x` itself. In other words, if we have a ring in which adding any element to itself results in the additive identity (zero), then negating any element in this ring gives us the original element back.
More concisely: In a ring of characteristic 2, the additive inverse of any element is equal to the element itself.
|
Mathlib.Algebra.CharP.Two._auxLemma.1
theorem Mathlib.Algebra.CharP.Two._auxLemma.1 : ∀ {M : Type u} [inst : Monoid M] (a : M), a * a = a ^ 2
This theorem, `Mathlib.Algebra.CharP.Two._auxLemma.1`, states that for any type `M` that has a `Monoid` instance and for any element `a` of type `M`, the result of multiplying `a` by itself is equivalent to `a` raised to the power of 2. In mathematical terms, for any monoid `M` and any element `a` in `M`, we have $a * a = a^2$.
More concisely: For any monoid `M` and element `a` in `M`, the product of `a` with itself equals the square of `a`, i.e., `a * a = a^2`.
|