RingInvoClass.involution
theorem RingInvoClass.involution :
∀ {F : Type u_2} {R : Type u_3} [inst : Semiring R] [inst_1 : EquivLike F R Rᵐᵒᵖ] [self : RingInvoClass F R] (f : F)
(x : R), (f (f x).unop).unop = x
This theorem states that for every ring involution, it must be its own inverse. More specifically, given any semiring `R`, and any `F` that is equivalent to the ring of opposites of `R`, and any ring involution on this set up, for any element `x` of `R`, applying the involution twice (i.e., `f (f x)`) gives back `x`. In other words, the involution undoes itself when applied twice. This is a fundamental property of ring involutions.
More concisely: For any ring involution `f` on a semiring `R`, `f (f x) = x` for all `x` in `R`.
|
RingInvo.involution'
theorem RingInvo.involution' :
∀ {R : Type u_1} [inst : Semiring R] (self : RingInvo R) (x : R), (self.toFun (self.toFun x).unop).unop = x := by
sorry
This theorem states that for any type `R` that is a semiring, and any ring involution (a function that is its own inverse) `self` on `R`, the function `self` is indeed an involution. Specifically, for any element `x` of `R`, applying the function `self` twice (i.e., `self.toFun (self.toFun x).unop`), and then applying the unary operation `unop`, results in the original element `x`. In mathematical terms, this means that the ring involution `self` is such that `self(self(x)) = x` for all `x` in `R`.
More concisely: For any semiring `R` and ring involution `self` on `R`, `self(self(x)) = x` for all `x` in `R`.
|