IsIdempotentElem.one_sub
theorem IsIdempotentElem.one_sub :
∀ {R : Type u_6} [inst : NonAssocRing R] {p : R}, IsIdempotentElem p → IsIdempotentElem (1 - p)
The theorem `IsIdempotentElem.one_sub` states that for any type `R` that forms a non-associative ring, and for any element `p` of `R`, if `p` is an idempotent element (meaning `p * p = p`), then the element `1 - p` is also idempotent. In mathematical terms, it states that if `p` is such that `p^2 = p`, then `(1 - p)^2 = 1 - p`.
More concisely: If `p` is an idempotent element in a non-associative ring `R`, then `1 - p` is also an idempotent element in `R` (i.e., `(1 - p)^2 = 1 - p`).
|
IsIdempotentElem.eq
theorem IsIdempotentElem.eq : ∀ {M : Type u_1} [inst : Mul M] {p : M}, IsIdempotentElem p → p * p = p
This theorem states that for any type `M` equipped with a multiplication operation, if an element `p` of `M` is idempotent (which means that `p * p = p`), then the theorem guarantees that indeed `p * p = p`. In essence, it confirms the property defined by `IsIdempotentElem`, which is being true for idempotent elements.
More concisely: If `M` is a type with multiplication and `p` is an idempotent element in `M` (i.e., `p * p = p`), then `p * p` equals `p`.
|
IsIdempotentElem.one
theorem IsIdempotentElem.one : ∀ {M₁ : Type u_5} [inst : MulOneClass M₁], IsIdempotentElem 1
This theorem states that, for any type `M₁` that is endowed with a multiplication and identity element (`MulOneClass M₁`), the number 1 is an idempotent element. In other words, when 1 is multiplied by itself, the result is 1. This is expressed mathematically as `1 * 1 = 1`.
More concisely: For any type `M₁` with multiplication and identity element, the identity element 1 is idempotent, i.e., `1 * 1 = 1`.
|