add_left_iterate
theorem add_left_iterate :
∀ {G : Type u_3} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => a + x)^[n] = fun x => n • a + x
This theorem states that for any type `G` that has an addition operation and an identity element (i.e., is an additive monoid), any element `a` from `G`, and any natural number `n`, applying the function that adds `a` to its input `n` times is the same as adding `n` times `a` to the input. In mathematical terms, for any `a` in `G` and `n` in ℕ, (a + x) iterated `n` times is the same as `n` • `a` + `x`, where '•' denotes scalar multiplication and 'x' is a variable.
More concisely: For any additive monoid `G` and its element `a`, natural number `n`, the operation of adding `a` to a value `x` `n` times is equivalent to adding `n` copies of `a` to `x`.
|
vadd_iterate
theorem vadd_iterate :
∀ {G : Type u_3} {H : Type u_4} [inst : AddMonoid G] (a : G) (n : ℕ) [inst_1 : AddAction G H],
(fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
This theorem states that for any type `G` with an `AddMonoid` structure (a set equipped with an associative addition operation and an additive identity element), a term `a` of type `G`, and a natural number `n`, along with any type `H` that has an `AddAction` of `G` on `H` (a representation of the concept of scalar multiplication), iterating the function `(fun x => a +ᵥ x)` `n` times is equivalent to the function that maps `x` to the scalar multiple `n • a +ᵥ x`. In simpler terms, it says that adding `a` to `x` `n` times is the same as multiplying `a` by `n` and then adding the result to `x`.
More concisely: For any additive monoid `G`, any `a : G`, natural number `n`, and any type `H` with an additive action of `G` on `H`, the function `(fun x => a +ᵥ x)` applied `n` times is equivalent to the function that maps `x` to `n • a +ᵥ x`. In other words, `(a +ᵥ _) ^ n = (fun x => n • a +ᵥ x)`.
|
pow_iterate
theorem pow_iterate : ∀ {G : Type u_3} [inst : Monoid G] (n j : ℕ), (fun x => x ^ n)^[j] = fun x => x ^ n ^ j := by
sorry
This theorem states that for any type `G` that forms a monoid, and for any two natural numbers `n` and `j`, the `j`-th iterate of the function that raises its argument to the `n`-th power is the same as the function that raises its argument to the power of `n` raised to the `j`-th power. In mathematical terms, for any element `x` in `G`, we have $(x^n)^j = x^{n^j}$.
More concisely: For any monoid `G` and natural numbers `n` and `j`, the `j`-th power of `n` applied to an element `x` in `G` is equal to the `j`-th iterate of the function that maps an element to its `n`-th power, i.e., $(x^n)^j = x^{n^j}$.
|
mul_right_iterate
theorem mul_right_iterate :
∀ {G : Type u_3} [inst : Monoid G] (a : G) (n : ℕ), (fun x => x * a)^[n] = fun x => x * a ^ n
This theorem states that for any type `G` that is a monoid and any element `a` of type `G`, if we apply the function that multiplies `x` by `a` `n` times (`(fun x => x * a)^[n]`), it is equivalent to multiplying `x` by `a` raised to the power of `n` (`fun x => x * a ^ n`). Basically, in a monoid, iteratively multiplying by `a` `n` times is the same as multiplying once by `a` to the power `n`.
More concisely: For any monoid `G` and element `a` in `G`, the repeated multiplication `(a * _)^[n]` is equal to the power multiplication `(a ^ n) * _`, where `_` is an arbitrary element of `G`.
|
hom_coe_pow
theorem hom_coe_pow :
∀ {M : Type u_1} {F : Type u_5} [inst : Monoid F] (c : F → M → M),
c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = (c f)^[n]
This theorem, `hom_coe_pow`, asserts that for any types `M` and `F`, where `F` is a monoid, and for any function `c` from `F` and `M` to `M` that satisfies two particular properties. The first property is that applying `c` to the identity element of `F` returns the identity function on `M`. The second property is that for any two elements `f` and `g` of `F`, applying `c` to the product of `f` and `g` is equivalent to first applying `c` to `g` and then applying `c` to `f`. Under these conditions, the theorem states that for any element `f` of `F` and any natural number `n`, applying `c` to `f` raised to the power `n` is equivalent to applying `c` to `f` `n` times.
More concisely: For any monoid `F` and function `c` from `F` and a type `M` such that applying `c` to the identity element is the identity function and applying `c` to the product of two elements is equivalent to applying `c` to the elements in order, applying `c` to an element `f` raised to a natural number `n` is equivalent to applying `c` to `f` `n` times.
|
mul_left_iterate
theorem mul_left_iterate :
∀ {G : Type u_3} [inst : Monoid G] (a : G) (n : ℕ), (fun x => a * x)^[n] = fun x => a ^ n * x
This theorem states that for any type `G` that has a Monoid structure, for any element `a` of `G` and for any natural number `n`, iterating the function `(fun x => a * x)` `n` times is the same as the function that multiplies `a` raised to the power of `n` by `x`. This is essentially expressing a property of exponentiation in the context of monoids.
More concisely: For any monoid `G` and element `a` in `G`, the repeated application of the function `x => a * x` in `G` `n` times is equivalent to the monoid multiplication of `a` raised to the power of `n` and `x`.
|
smul_iterate
theorem smul_iterate :
∀ {G : Type u_3} {H : Type u_4} [inst : Monoid G] (a : G) (n : ℕ) [inst_1 : MulAction G H],
(fun x => a • x)^[n] = fun x => a ^ n • x
This theorem, `smul_iterate`, states that for any type `G` with a monoid structure, a value `a` of type `G`, a natural number `n`, and any type `H` with a multiplication action defined by `G`, the `n`-th iterate of the function that scales by `a` is equivalent to the function that scales by `a` raised to the power of `n`. In other words, applying the scaling function `n` times in a row has the same effect as scaling once by `a^n`.
More concisely: For any monoid `G` and element `a` in `G`, any type `H` with a right action by `G`, and natural number `n`, the repeated application of the function that scales elements in `H` by `a` is equivalent to scaling them by `a` raised to the power of `n`.
|
add_right_iterate
theorem add_right_iterate :
∀ {G : Type u_3} [inst : AddMonoid G] (a : G) (n : ℕ), (fun x => x + a)^[n] = fun x => x + n • a
This theorem, named `add_right_iterate`, states that for any type `G` that forms an additive monoid and any element `a` of type `G` and natural number `n`, iterating the function of adding `a` to another element `x` `n` times is equivalent to the function of adding `n` times `a` to `x`. Essentially, it's expressing the distributive property of addition over scalar multiplication in terms of function iteration.
More concisely: For any additive monoid `G` and `a` in `G` and natural number `n`, the function `iterate (λ x, x + a) n` equals the function `λ x, (n • a) + x`.
|