Instances on spaces of monoid and group morphisms #

This file does two things involving AddMonoid.End and Ring. They are separate, and if someone would like to split this file in two that may be helpful.

theorem AddMonoid.End.natCast_apply {M : Type uM} [AddCommMonoid M] (n : ) (m : M) :
n m = n m

See also AddMonoid.End.natCast_def.

theorem AddMonoid.End.ofNat_apply {M : Type uM} [AddCommMonoid M] (n : ) [n.AtLeastTwo] (m : M) :
(OfNat.ofNat n) m = n m
  • One or more equations did not get rendered due to their size.
  • AddMonoid.End.instRing = let __src := AddMonoid.End.instSemiring; let __src_1 := AddMonoid.End.instAddCommGroup; SubNegMonoid.zsmul

Miscellaneous definitions #

This file used to import Algebra.GroupPower.Basic, hence it was not possible to import it in some of the lower-level files like Algebra.Ring.Basic. The following lemmas should be rehomed now that Algebra.GroupPower.Basic was deleted.

Multiplication of an element of a (semi)ring is an AddMonoidHom in both arguments.

This is a more-strongly bundled version of AddMonoidHom.mulLeft and AddMonoidHom.mulRight.

Stronger versions of this exists for algebras as LinearMap.mul, NonUnitalAlgHom.mul and Algebra.lmul.

  • AddMonoidHom.mul = { toFun := AddMonoidHom.mulLeft, map_zero' := , map_add' := }
Instances For
    theorem AddMonoidHom.mul_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : R) (y : R) :
    (AddMonoidHom.mul x) y = x * y
    theorem AddMonoidHom.coe_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] :
    AddMonoidHom.mul = AddMonoidHom.mulLeft
    theorem AddMonoidHom.coe_flip_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] :
    AddMonoidHom.mul.flip = AddMonoidHom.mulRight
    theorem AddMonoidHom.map_mul_iff {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [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

    An AddMonoidHom preserves multiplication if pre- and post- composition with AddMonoidHom.mul are equivalent. By converting the statement into an equality of AddMonoidHoms, this lemma allows various specialized ext lemmas about →+ to then be applied.

    theorem AddMonoid.End.mulLeft_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) :
    ∀ (x : R), (AddMonoid.End.mulLeft r) x = r * x

    The left multiplication map: (a, b) ↦ a * b. See also AddMonoidHom.mulLeft.

    • AddMonoid.End.mulLeft = AddMonoidHom.mul
    Instances For
      theorem AddMonoid.End.mulRight_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (y : R) (x : R) :
      (AddMonoid.End.mulRight y) x = x * y

      The right multiplication map: (a, b) ↦ b * a. See also AddMonoidHom.mulRight.

      • AddMonoid.End.mulRight = AddMonoidHom.mul.flip
      Instances For
        theorem AddMonoid.End.mulRight_eq_mulLeft {R : Type u_1} [NonUnitalNonAssocCommSemiring R] :
        AddMonoid.End.mulRight = AddMonoid.End.mulLeft