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.

• We provide the Ring structure on AddMonoid.End.
• Results about AddMonoid.End R when R is a ring.

instance AddMonoid.End.instAddMonoidWithOne (M : Type u_1) [AddCommMonoid M] : AddMonoidWithOne (AddMonoid.End M)

Equations

• AddMonoid.End.instAddMonoidWithOne M = AddMonoidWithOne.mk ⋯ ⋯

@[simp]

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

See also AddMonoid.End.natCast_def.

@[simp]

theorem AddMonoid.End.ofNat_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) [Nat.AtLeastTwo n] (m : M) : (OfNat.ofNat n) m = n • m

instance AddMonoid.End.instSemiring {M : Type uM} [AddCommMonoid M] : Semiring (AddMonoid.End M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoid.End.instRing {M : Type uM} [AddCommGroup M] : Ring (AddMonoid.End M)

Equations

• AddMonoid.End.instRing = let __src := AddMonoid.End.instSemiring; let __src_1 := AddMonoid.End.instAddCommGroup; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Miscellaneous definitions

Due to the fact this file imports Algebra.GroupPower.Basic, it is not possible to import it in some of the lower-level files like Algebra.Ring.Basic. The following lemmas should be rehomed if the import structure permits them to be.

def AddMonoidHom.mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R

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.

Equations

• AddMonoidHom.mul = { toZeroHom := { toFun := AddMonoidHom.mulLeft, map_zero' := ⋯ }, map_add' := ⋯ }

theorem AddMonoidHom.mul_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : R) (y : R) : (AddMonoidHom.mul x) y = x * y

@[simp]

theorem AddMonoidHom.coe_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑AddMonoidHom.mul = AddMonoidHom.mulLeft

@[simp]

theorem AddMonoidHom.coe_flip_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑(AddMonoidHom.flip AddMonoidHom.mul) = 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.compr₂ AddMonoidHom.mul f = AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul f) 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 AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {a : R} : AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ↔ ∀ (b : R), Commute a b

theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {b : R} : AddMonoidHom.mulRight b = AddMonoidHom.mulLeft b ↔ ∀ (a : R), Commute a b

@[simp]

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

def AddMonoid.End.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

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

Equations

• AddMonoid.End.mulLeft = AddMonoidHom.mul

@[simp]

theorem AddMonoid.End.mulRight_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (y : R) (x : R) : (AddMonoid.End.mulRight y) x = x * y

def AddMonoid.End.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

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

Equations

• AddMonoid.End.mulRight = AddMonoidHom.flip AddMonoidHom.mul

theorem AddMonoid.End.mulRight_eq_mulLeft {R : Type u_1} [NonUnitalNonAssocCommSemiring R] : AddMonoid.End.mulRight = AddMonoid.End.mulLeft