SymAlg.sym_injective
theorem SymAlg.sym_injective : ∀ {α : Type u_1}, Function.Injective ⇑SymAlg.sym
The theorem `SymAlg.sym_injective` states that for all types `α`, the function `SymAlg.sym` is injective. In other words, given any two elements of type `α`, if applying `SymAlg.sym` to both yields the same result, this implies that the original elements were equal. In mathematical terms, if `SymAlg.sym a₁ = SymAlg.sym a₂` then `a₁ = a₂`.
More concisely: For all types `α`, the function `SymAlg.sym` is an injection from `α` to itself.
|
SymAlg.unsym_zero
theorem SymAlg.unsym_zero : ∀ {α : Type u_1} [inst : Zero α], SymAlg.unsym 0 = 0
This theorem states that for any type `α` that has a zero element (i.e., for any type `α` equipped with a zero structure), the unsym operation (which retrieves the element of `α` represented by an element in the symmetric algebra `αˢʸᵐ`) applied to the zero element of the symmetric algebra results in the zero element of `α`. In other words, unsym maps the zero of the symmetric algebra to the zero of the original type `α`.
More concisely: For any type `α` with a zero element, the unsym operation in the symmetric algebra maps the zero of the symmetric algebra to the zero of `α`.
|
SymAlg.mul_def
theorem SymAlg.mul_def :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Mul α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
(a b : αˢʸᵐ), a * b = SymAlg.sym (⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a))
This theorem states that for any type `α` that has addition, multiplication, a specified unity ("one"), a way to interpret the number 2, and an invertible 2, and any two elements `a` and `b` of the symbolic algebra of `α`, the product of `a` and `b` in the symbolic algebra is represented by the element of `α` which is the average (multiplied by the multiplicative inverse of 2) of the product of the elements represented by `a` and `b` and the product of the elements represented by `b` and `a`. In other words, in this symbolic algebra, multiplication is commutative and averaged.
More concisely: For any commutative ring `α` with unity and invertible 2, the multiplication is distributive over averaging, that is, `(a * b) + (b * a) = (a + b) * (a ^ (-1) + b ^ (-1))` for all `a, b` in `α`.
|
SymAlg.unsym_add
theorem SymAlg.unsym_add :
∀ {α : Type u_1} [inst : Add α] (a b : αˢʸᵐ), SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b
The theorem `SymAlg.unsym_add` states that for any type `α` that has an addition operation, and for any two symbolic elements `a` and `b` of this type, the unsymbolization of the sum of `a` and `b` is the same as the sum of the unsymbolized `a` and the unsymbolized `b`. In other words, the `unsym` operation commutes with the `+` operation.
More concisely: For any type `α` with addition and for all `a, b : α`, the unsymbolic representation of `a + b` is equal to the unsymbolic representation of `a + b`.
|
SymAlg.unsym_injective
theorem SymAlg.unsym_injective : ∀ {α : Type u_1}, Function.Injective ⇑SymAlg.unsym
The theorem `SymAlg.unsym_injective` states that for any type `α`, the function 'unsym' from the symbolic algebra `SymAlg` is injective. In other words, for every pair of elements in the symbolic algebra, if applying 'unsym' to them yields the same result, then the original elements were identical. This reflects the property of injective functions where if the outputs are the same, the inputs must also be the same.
More concisely: The `SymAlg.unsym` function in Lean 4 maps distinct elements of the symbolic algebra to distinct results.
|
SymAlg.sym_mul_sym
theorem SymAlg.sym_mul_sym :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
(a b : α), SymAlg.sym a * SymAlg.sym b = SymAlg.sym (⅟2 * (a * b + b * a))
The theorem `SymAlg.sym_mul_sym` states that for any type `α` equipped with multiplication, addition, a one element, a representation of the natural number 2, and where 2 is invertible, the product of the symmetric algebra elements corresponding to `a` and `b` (denoted `SymAlg.sym a` and `SymAlg.sym b` respectively) is equal to the symmetric algebra element corresponding to half of the sum of `a * b` and `b * a` (denoted `SymAlg.sym (⅟2 * (a * b + b * a))`).
More concisely: For any type `α` with multiplication, addition, a one element, a representation of 2, and 2 invertible, `SymAlg.sym (a * b) = SymAlg.sym (⅟2 * (a * b + b * a))` for all `a, b : α`.
|