Algebraic identities and operations

Polynomial and product identities, sum-of-squares identities, functional equations on rings, and elementary operations on functions and sets.

TheoremCandido's identity#✓fully proved

For all elements \(x\) and \(y\) of a commutative semiring, \(2\left(x^4 + y^4 + (x + y)^4\right) = \left(x^2 + y^2 + (x + y)^2\right)^2\).

theorem candido_identity {R : Type*} [CommSemiring R] (x y : R) :
    2 * (x ^ 4 + y ^ 4 + (x + y) ^ 4) = (x ^ 2 + y ^ 2 + (x + y) ^ 2) ^ 2
Sources

DefinitionIndicator function of a set#✓fully proved

For a set \(A \subseteq \alpha\) and a type \(R\) with a zero and a one, the indicator function \(\mathbb{1}_A : \alpha \to R\) takes the value \(1\) at every point of \(A\) and the value \(0\) at every point outside \(A\).

noncomputable def indicatorOne : α → R := indicator A (fun _ ↦ 1)

DefinitionL-additive functions on a ring#✓fully proved

A function \(f \colon K \to K\) on a ring \(K\) is L-additive when \(f(mn) = f(m)\,n + f(n)\,m\) for all \(m, n \in K\).

def IsLAdditive {K : Type*} [Ring K] (f : K → K) : Prop :=
  ∀ m n, f (m * n) = f m * n + f n * m

TheoremProducts regrouped by the values of a function#✓fully proved

Let \(\beta\) and \(\gamma\) be finite types, let \(M\) be a commutative monoid, and let \(g : \beta \to \gamma\) and \(f : \gamma \to M\). Then

\[\prod_{b \in \beta} f(g(b)) = \prod_{c \in \gamma} f(c)^{\#\{b \in \beta \mid g(b) = c\}},\]

where the product on the right runs over all of \(\gamma\) and \(\#\{b \in \beta \mid g(b) = c\}\) is the number of elements \(b\) of \(\beta\) with \(g(b) = c\).

theorem prod_comp_eq_prod_pow {β γ M : Type*} [Fintype β] [Fintype γ] [DecidableEq γ]
    [CommMonoid M] (g : β → γ) (f : γ → M) :
    ∏ b, f (g b) = ∏ c, f c ^ (univ.filter fun b => g b = c).card
Used by 1
Used byThe sequence likelihood depends only on the label counts
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.