AddMonoidAlgebra.divOf_add_modOf
theorem AddMonoidAlgebra.divOf_add_modOf :
∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCancelCommMonoid G] (x : AddMonoidAlgebra k G)
(g : G), AddMonoidAlgebra.of' k G g * x.divOf g + x.modOf g = x
This theorem states that for any semiring `k` and any add-cancel-commutative monoid `G`, for any element `x` in the monoid algebra of `G` over `k` and any element `g` in `G`, if we multiply the embedding of `g` in the monoid algebra by the division of `x` by the embedding of `g`, then add the remainder of `x` divided by the embedding of `g`, we get back `x`. This is a division algorithm in the monoid algebra, analogous to the division algorithm in the integers where `a = bq + r` for integers `a, b, q, r` with `r < b`.
More concisely: For any semiring `k` and add-cancel-commutative monoid `G`, the division algorithm holds in the monoid algebra over `k`: for all `x` in the monoid algebra and `g` in `G`, there exist unique elements `q` and `r` in the monoid algebra such that `x = g * q + r` and `r = 0` or `r` is the remainder of the division of `x` by `g`, with degree of `r` strictly less than the degree of `g`.
|
AddMonoidAlgebra.divOf_apply
theorem AddMonoidAlgebra.divOf_apply :
∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCancelCommMonoid G] (g : G)
(x : AddMonoidAlgebra k G) (g' : G), (x.divOf g) g' = x (g + g')
The theorem `AddMonoidAlgebra.divOf_apply` states that for any types `k` and `G` where `k` is a semiring and `G` is an additive cancel commutative monoid, given elements `g` and `g'` of `G` and an element `x` of the monoid algebra of `G` over `k`, applying the `divOf` function to `x` and `g`, and then applying the result to `g'`, is equal to applying `x` to the sum of `g` and `g'`. In other words, the operation of dividing by a given term `g` in the monoid algebra and then applying the result to another term `g'` is the same as applying the original element of the monoid algebra to the sum of the two terms `g` and `g'`.
More concisely: For any semiring `k` and additive cancel commutative monoid `G`, the operation of dividing an element `x` of the monoid algebra of `G` over `k` by an element `g` of `G` and then applying the result to another element `g'` of `G`, is equivalent to applying `x` to the sum of `g` and `g'`.
|
AddMonoidAlgebra.modOf_apply_of_not_exists_add
theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add :
∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCancelCommMonoid G] (x : AddMonoidAlgebra k G)
(g g' : G), (¬∃ d, g' = g + d) → (x.modOf g) g' = x g'
The theorem `AddMonoidAlgebra.modOf_apply_of_not_exists_add` states that for any type `k` with a semiring structure, any type `G` with an addition-commutative cancelable monoid structure, an instance of the monoid algebra `x` generated by `G` over `k`, and two elements `g` and `g'` from `G`, if there does not exist an element `d` in `G` such that `g'` is the sum of `g` and `d`, then applying the function `AddMonoidAlgebra.modOf` with `g` on `x` and then applying the resulting function on `g'` is equal to the application of `x` on `g'`. In other words, the function `AddMonoidAlgebra.modOf` leaves the coefficient of `g'` in the algebra `x` unchanged if `g'` cannot be expressed as the sum of `g` and another element.
More concisely: If `g'` is not the sum of `g` in the additive monoid `G`, then applying `AddMonoidAlgebra.modOf` with `g` on the monoid algebra `x` over `k` leaves the coefficient of `g'` unchanged.
|
AddMonoidAlgebra.modOf_apply_self_add
theorem AddMonoidAlgebra.modOf_apply_self_add :
∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCancelCommMonoid G] (x : AddMonoidAlgebra k G)
(g d : G), (x.modOf g) (g + d) = 0
This theorem states that for any semiring `k`, any additive cancel commutative monoid `G`, any element `x` of the monoid algebra of `G` over `k`, and any elements `g` and `d` of `G`, the value at `g + d` of the monoid algebra element obtained by reducing `x` modulo `g` is zero. In other words, when you take an element of the monoid algebra, reduce it modulo another element of the monoid, and then evaluate this at the sum of the original element and another element, the result is always zero. This essentially captures a property of the modulo operation in the context of monoid algebras.
More concisely: For any semiring `k`, additive cancel commutative monoid `G`, and elements `x` in the monoid algebra of `G` over `k`, `g`, `d` in `G`, the evaluation of `x` reduced modulo `g` at `g + d` is equal to zero.
|
AddMonoidAlgebra.modOf_apply_of_exists_add
theorem AddMonoidAlgebra.modOf_apply_of_exists_add :
∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCancelCommMonoid G] (x : AddMonoidAlgebra k G)
(g g' : G), (∃ d, g' = g + d) → (x.modOf g) g' = 0
The theorem `AddMonoidAlgebra.modOf_apply_of_exists_add` asserts that for any semiring `k`, any additive cancel commutative monoid `G`, any element `x` from the monoid algebra of `G` over `k`, and any elements `g` and `g'` from `G`, if there exists a member `d` from `G` such that `g'` is the sum of `g` and `d`, then the application of the function `AddMonoidAlgebra.modOf x g` to `g'` yields zero. In other words, if `g'` can be written as `g` plus some element, then `g'` gets mapped to zero by the "modulus" operation `AddMonoidAlgebra.modOf x g` in the monoid algebra.
More concisely: For any semiring `k`, additive cancel commutative monoid `G`, element `x` in the monoid algebra of `G` over `k`, and elements `g` and `g'` in `G`, if there exists `d` in `G` such that `g' = g + d`, then `AddMonoidAlgebra.modOf x g (g') = 0`.
|
AddMonoidAlgebra.divOf.proof_1
theorem AddMonoidAlgebra.divOf.proof_1 :
∀ {G : Type u_1} [inst : AddCancelCommMonoid G] (g : G), Function.Injective fun x => g + x
The theorem `AddMonoidAlgebra.divOf.proof_1` states that for any type `G` that forms an additive cancellative commutative monoid (i.e., a structure where addition operation is associative, commutative, and has an identity, and moreover, every element has an additive inverse), every element `g` of `G` gives rise to a function that adds `g` to its input. This function is injective. In mathematical terms, this means for all `g`, the function `f(x) = g + x` is such that if `f(x) = f(y)`, then `x = y`.
More concisely: For every additive cancellative commutative monoid `G`, the function `x => g + x` is an injection from `G` to itself for any `g` in `G`.
|