AddMonoidHom.map_mul_iff
theorem AddMonoidHom.map_mul_iff :
∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
(f : R →+ S),
(∀ (x y : R), f (x * y) = f x * f y) ↔ AddMonoidHom.mul.compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f
This theorem establishes a condition for a homomorphism between additive monoids (`AddMonoidHom`) to preserve multiplication. Specifically, for any two types `R` and `S` that form non-unital and non-associative semirings, if we have an `AddMonoidHom` `f` from `R` to `S`, then `f` preserves multiplication (i.e., `f(x * y) = f(x) * f(y)` for any `x` and `y` in `R`) if and only if the composition of `AddMonoidHom.mul` and `f` in both directions (pre-composition and post-composition) are equivalent. This allows the application of various specialized extensionality (`ext`) lemmas about `→+` once the statement is converted into an equality of `AddMonoidHoms`.
More concisely: A homomorphism between non-unital and non-associative semirings preserves multiplication if and only if it is equal to its own pre- and post-composition with the additive monoid multiplication.
|
AddMonoid.End.natCast_apply
theorem AddMonoid.End.natCast_apply : ∀ {M : Type uM} [inst : AddCommMonoid M] (n : ℕ) (m : M), ↑n m = n • m
This theorem, `AddMonoid.End.natCast_apply`, states that for any given type `M` that forms an additive commutative monoid, and for any natural number `n` and element `m` of type `M`, the application of the "coercion" or "cast" of `n` to `m` is equivalent to the scalar multiplication of `n` and `m`. In simpler terms, it means that casting a natural number `n` to an endomorphism on `M` and applying it to an element `m` of `M` is the same as multiplying `m` by `n`.
More concisely: For any additive commutative monoid type `M` and natural number `n`, the coercion of `n` to an endomorphism of `M` and application to an element `m` is equal to scalar multiplication of `m` by `n`.
|