Mathlib.Algebra.Ring.Pi

Pi.distrib instance

[∀ i, Distrib <| f i] : Distrib (∀ i : I, f i)

Full source

instance distrib [∀ i, Distrib <| f i] : Distrib (∀ i : I, f i) :=
  { add := (· + ·)
    mul := (· * ·)
    left_distrib := by intros; ext; exact mul_add _ _ _
    right_distrib := by intros; ext; exact add_mul _ _ _}

Distributivity of Pointwise Multiplication in Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ has a distributive multiplication over addition, the product type $\prod_{i \in I} f_i$ inherits a pointwise multiplication operation that is distributive over addition. That is, for any $x, y, z \in \prod_{i \in I} f_i$, we have $x \cdot (y + z) = x \cdot y + x \cdot z$ and $(x + y) \cdot z = x \cdot z + y \cdot z$ componentwise.

Pi.hasDistribNeg instance

[∀ i, Mul (f i)] [∀ i, HasDistribNeg (f i)] : HasDistribNeg (∀ i, f i)

Full source

instance hasDistribNeg [∀ i, Mul (f i)] [∀ i, HasDistribNeg (f i)] : HasDistribNeg (∀ i, f i) where
  neg_mul _ _ := funext fun _ ↦ neg_mul _ _
  mul_neg _ _ := funext fun _ ↦ mul_neg _ _

Distributive Negation on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation and a negation operation that distributes over multiplication, the product type $\prod_{i \in I} f_i$ inherits a pointwise negation operation that distributes over the pointwise multiplication. That is, for any $x, y \in \prod_{i \in I} f_i$, we have $-(x \cdot y) = (-x) \cdot y = x \cdot (-y)$ componentwise.

Pi.addMonoidWithOne instance

[∀ i, AddMonoidWithOne (f i)] : AddMonoidWithOne (∀ i, f i)

Full source

instance addMonoidWithOne [∀ i, AddMonoidWithOne (f i)] : AddMonoidWithOne (∀ i, f i) where
  natCast n _ := n
  natCast_zero := funext fun _ ↦ AddMonoidWithOne.natCast_zero
  natCast_succ n := funext fun _ ↦ AddMonoidWithOne.natCast_succ n

Pointwise Additive Monoid with One on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an additive monoid structure with a distinguished element $1$ and a canonical homomorphism from the natural numbers, the product type $\prod_{i \in I} f_i$ inherits an additive monoid structure with a distinguished element $1$ and a canonical homomorphism from the natural numbers, defined pointwise.

Pi.addGroupWithOne instance

[∀ i, AddGroupWithOne (f i)] : AddGroupWithOne (∀ i, f i)

Full source

instance addGroupWithOne [∀ i, AddGroupWithOne (f i)] : AddGroupWithOne (∀ i, f i) where
  __ := addGroup
  __ := addMonoidWithOne
  intCast n _ := n
  intCast_ofNat n := funext fun _ ↦ AddGroupWithOne.intCast_ofNat n
  intCast_negSucc n := funext fun _ ↦ AddGroupWithOne.intCast_negSucc n

Pointwise Additive Group with One on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an additive group structure with a distinguished element $1$ and canonical homomorphisms from the integers, the product type $\prod_{i \in I} f_i$ inherits an additive group structure with a distinguished element $1$ and canonical homomorphisms from the integers, defined pointwise.

Pi.nonUnitalNonAssocSemiring instance

[∀ i, NonUnitalNonAssocSemiring <| f i] : NonUnitalNonAssocSemiring (∀ i : I, f i)

Full source

instance nonUnitalNonAssocSemiring [∀ i, NonUnitalNonAssocSemiring <| f i] :
    NonUnitalNonAssocSemiring (∀ i : I, f i) :=
  { Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }

Pointwise Non-unital Non-associative Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital non-associative semiring, the product type $\prod_{i \in I} f_i$ inherits a non-unital non-associative semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.nonUnitalSemiring instance

[∀ i, NonUnitalSemiring <| f i] : NonUnitalSemiring (∀ i : I, f i)

Full source

instance nonUnitalSemiring [∀ i, NonUnitalSemiring <| f i] : NonUnitalSemiring (∀ i : I, f i) :=
  { Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }

Pointwise Non-unital Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital semiring, the product type $\prod_{i \in I} f_i$ inherits a non-unital semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication is associative and distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.nonAssocSemiring instance

[∀ i, NonAssocSemiring <| f i] : NonAssocSemiring (∀ i : I, f i)

Full source

instance nonAssocSemiring [∀ i, NonAssocSemiring <| f i] : NonAssocSemiring (∀ i : I, f i) :=
  { Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }

Pointwise Non-associative Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-associative semiring, the product type $\prod_{i \in I} f_i$ inherits a non-associative semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.semiring instance

[∀ i, Semiring <| f i] : Semiring (∀ i : I, f i)

Full source

instance semiring [∀ i, Semiring <| f i] : Semiring (∀ i : I, f i) :=
  { Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }

Pointwise Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a semiring, the product type $\prod_{i \in I} f_i$ inherits a semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication is associative and distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.nonUnitalCommSemiring instance

[∀ i, NonUnitalCommSemiring <| f i] : NonUnitalCommSemiring (∀ i : I, f i)

Full source

instance nonUnitalCommSemiring [∀ i, NonUnitalCommSemiring <| f i] :
    NonUnitalCommSemiring (∀ i : I, f i) :=
  { Pi.nonUnitalSemiring, Pi.commSemigroup with }

Pointwise Non-unital Commutative Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital commutative semiring, the product type $\prod_{i \in I} f_i$ inherits a non-unital commutative semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication is commutative and associative componentwise - Multiplication distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.commSemiring instance

[∀ i, CommSemiring <| f i] : CommSemiring (∀ i : I, f i)

Full source

instance commSemiring [∀ i, CommSemiring <| f i] : CommSemiring (∀ i : I, f i) :=
  { Pi.semiring, Pi.commMonoid with }

Pointwise Commutative Semiring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative semiring, the product type $\prod_{i \in I} f_i$ inherits a commutative semiring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication is commutative, associative, and distributes over addition componentwise - Multiplication by zero annihilates componentwise

Pi.nonUnitalNonAssocRing instance

[∀ i, NonUnitalNonAssocRing <| f i] : NonUnitalNonAssocRing (∀ i : I, f i)

Full source

instance nonUnitalNonAssocRing [∀ i, NonUnitalNonAssocRing <| f i] :
    NonUnitalNonAssocRing (∀ i : I, f i) :=
  { Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }

Pointwise Non-unital Non-associative Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital non-associative ring, the product type $\prod_{i \in I} f_i$ inherits a non-unital non-associative ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication distributes over addition componentwise

Pi.nonUnitalRing instance

[∀ i, NonUnitalRing <| f i] : NonUnitalRing (∀ i : I, f i)

Full source

instance nonUnitalRing [∀ i, NonUnitalRing <| f i] : NonUnitalRing (∀ i : I, f i) :=
  { Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }

Pointwise Non-unital Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital ring, the product type $\prod_{i \in I} f_i$ inherits a non-unital ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication is associative and distributes over addition componentwise

Pi.nonAssocRing instance

[∀ i, NonAssocRing <| f i] : NonAssocRing (∀ i : I, f i)

Full source

instance nonAssocRing [∀ i, NonAssocRing <| f i] : NonAssocRing (∀ i : I, f i) :=
  { Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }

Pointwise Non-associative Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-associative ring, the product type $\prod_{i \in I} f_i$ inherits a non-associative ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication distributes over addition componentwise - The element 1 acts as a multiplicative identity componentwise

Pi.ring instance

[∀ i, Ring <| f i] : Ring (∀ i : I, f i)

Full source

instance ring [∀ i, Ring <| f i] : Ring (∀ i : I, f i) :=
  { Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }

Pointwise Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a ring, the product type $\prod_{i \in I} f_i$ inherits a ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication is associative and distributes over addition componentwise - The element 1 acts as a multiplicative identity componentwise

Pi.nonUnitalCommRing instance

[∀ i, NonUnitalCommRing <| f i] : NonUnitalCommRing (∀ i : I, f i)

Full source

instance nonUnitalCommRing [∀ i, NonUnitalCommRing <| f i] : NonUnitalCommRing (∀ i : I, f i) :=
  { Pi.nonUnitalRing, Pi.commSemigroup with }

Pointwise Non-unital Commutative Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a non-unital commutative ring, the product type $\prod_{i \in I} f_i$ inherits a non-unital commutative ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero element is the function that returns the zero element of each $f_i$ - Multiplication is commutative and associative, and distributes over addition componentwise

Pi.commRing instance

[∀ i, CommRing <| f i] : CommRing (∀ i : I, f i)

Full source

instance commRing [∀ i, CommRing <| f i] : CommRing (∀ i : I, f i) :=
  { Pi.ring, Pi.commSemiring with }

Pointwise Commutative Ring Structure on Product Types

Informal description

For any indexed family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative ring, the product type $\prod_{i \in I} f_i$ inherits a commutative ring structure with pointwise operations. Specifically: - Addition and multiplication are defined componentwise - The additive inverse is defined componentwise - The zero and one elements are the functions that return the zero and one elements of each $f_i$ respectively - Multiplication is commutative, associative, and distributes over addition componentwise - The element 1 acts as a multiplicative identity componentwise

Pi.nonUnitalRingHom definition

 {γ : Type w} [∀ i, NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i) :
  γ →ₙ+* ∀ i, f i

Full source

/-- A family of non-unital ring homomorphisms `f a : γ →ₙ+* β a` defines a non-unital ring
homomorphism `Pi.nonUnitalRingHom f : γ →+* Π a, β a` given by
`Pi.nonUnitalRingHom f x b = f b x`. -/
@[simps]
protected def nonUnitalRingHom {γ : Type w} [∀ i, NonUnitalNonAssocSemiring (f i)]
    [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i) : γ →ₙ+* ∀ i, f i :=
  { Pi.mulHom fun i => (g i).toMulHom, Pi.addMonoidHom fun i => (g i).toAddMonoidHom with
    toFun := fun x b => g b x }

Product of non-unital ring homomorphisms

Informal description

Given a family of non-unital ring homomorphisms $g_i : \gamma \to f_i$ for each index $i$, where $\gamma$ and each $f_i$ are non-unital non-associative semirings, the function $\text{Pi.nonUnitalRingHom}\, g : \gamma \to \prod_i f_i$ defined by $(\text{Pi.nonUnitalRingHom}\, g)(x)_i = g_i(x)$ is a non-unital ring homomorphism. This combines the multiplicative and additive homomorphism structures componentwise.

Pi.nonUnitalRingHom_injective theorem

 {γ : Type w} [Nonempty I] [∀ i, NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i)
  (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.nonUnitalRingHom g)

Full source

theorem nonUnitalRingHom_injective {γ : Type w} [Nonempty I]
    [∀ i, NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i)
    (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.nonUnitalRingHom g) :=
  mulHom_injective (fun i => (g i).toMulHom) hg

Injectivity of Product of Non-unital Ring Homomorphisms

Informal description

Let $I$ be a nonempty index set, and for each $i \in I$, let $f_i$ be a non-unital non-associative semiring. Let $\gamma$ be another non-unital non-associative semiring. Given a family of injective non-unital ring homomorphisms $g_i \colon \gamma \to f_i$ for each $i \in I$, the product homomorphism $\prod_i g_i \colon \gamma \to \prod_i f_i$ defined by $(\prod_i g_i)(x)_i = g_i(x)$ is also injective.

Pi.ringHom definition

{γ : Type w} [∀ i, NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : ∀ i, γ →+* f i) : γ →+* ∀ i, f i

Full source

/-- A family of ring homomorphisms `f a : γ →+* β a` defines a ring homomorphism
`Pi.ringHom f : γ →+* Π a, β a` given by `Pi.ringHom f x b = f b x`. -/
@[simps]
protected def ringHom {γ : Type w} [∀ i, NonAssocSemiring (f i)] [NonAssocSemiring γ]
    (g : ∀ i, γ →+* f i) : γ →+* ∀ i, f i :=
  { Pi.monoidHom fun i => (g i).toMonoidHom, Pi.addMonoidHom fun i => (g i).toAddMonoidHom with
    toFun := fun x b => g b x }

Product of ring homomorphisms

Informal description

Given a family of ring homomorphisms $ g_i \colon \gamma \to f_i $ for each index $ i $, where $\gamma$ and each $f_i$ are non-associative semirings, the function $\text{Pi.ringHom}\, g \colon \gamma \to \prod_i f_i$ defined by $(\text{Pi.ringHom}\, g)(x)_i = g_i(x)$ is a ring homomorphism. This combines the multiplicative and additive homomorphism structures componentwise.

Pi.ringHom_injective theorem

 {γ : Type w} [Nonempty I] [∀ i, NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : ∀ i, γ →+* f i)
  (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.ringHom g)

Full source

theorem ringHom_injective {γ : Type w} [Nonempty I] [∀ i, NonAssocSemiring (f i)]
    [NonAssocSemiring γ] (g : ∀ i, γ →+* f i) (hg : ∀ i, Function.Injective (g i)) :
    Function.Injective (Pi.ringHom g) :=
  monoidHom_injective (fun i => (g i).toMonoidHom) hg

Injectivity of Product of Ring Homomorphisms

Informal description

Let $I$ be a nonempty index set, and for each $i \in I$, let $f_i$ and $\gamma$ be non-associative semirings. Given a family of injective ring homomorphisms $g_i \colon \gamma \to f_i$ for each $i \in I$, the product homomorphism $\prod_i g_i \colon \gamma \to \prod_i f_i$ defined by $(\prod_i g_i)(x)_i = g_i(x)$ is injective.

Pi.evalNonUnitalRingHom definition

(f : I → Type v) [∀ i, NonUnitalNonAssocSemiring (f i)] (i : I) : (∀ i, f i) →ₙ+* f i

Full source

/-- Evaluation of functions into an indexed collection of non-unital rings at a point is a
non-unital ring homomorphism. This is `Function.eval` as a `NonUnitalRingHom`. -/
@[simps!]
def Pi.evalNonUnitalRingHom (f : I → Type v) [∀ i, NonUnitalNonAssocSemiring (f i)] (i : I) :
    (∀ i, f i) →ₙ+* f i :=
  { Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }

Evaluation as a non-unital ring homomorphism

Informal description

For an indexed family of non-unital non-associative semirings $(f_i)_{i \in I}$ and a fixed index $i \in I$, the evaluation map at $i$ is a non-unital ring homomorphism from the product $\prod_{i \in I} f_i$ to $f_i$. Specifically, the map sends a function $g$ to its value $g(i)$, and preserves both addition and multiplication.

Pi.constNonUnitalRingHom definition

(α β : Type*) [NonUnitalNonAssocSemiring β] : β →ₙ+* α → β

Full source

/-- `Function.const` as a `NonUnitalRingHom`. -/
@[simps]
def Pi.constNonUnitalRingHom (α β : Type*) [NonUnitalNonAssocSemiring β] : β →ₙ+* α → β :=
  { Pi.nonUnitalRingHom fun _ => NonUnitalRingHom.id β with toFun := Function.const _ }

Constant function as a non-unital ring homomorphism

Informal description

The constant function as a non-unital ring homomorphism. Given a non-unital non-associative semiring $\beta$ and any type $\alpha$, the function that maps every element of $\beta$ to the constant function $\alpha \to \beta$ (sending all inputs to that element) is a non-unital ring homomorphism from $\beta$ to the function space $\alpha \to \beta$ (where the latter has pointwise operations).

NonUnitalRingHom.compLeft definition

 {α β : Type*} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type*) :
  (I → α) →ₙ+* I → β

Full source

/-- Non-unital ring homomorphism between the function spaces `I → α` and `I → β`, induced by a
non-unital ring homomorphism `f` between `α` and `β`. -/
@[simps]
protected def NonUnitalRingHom.compLeft {α β : Type*} [NonUnitalNonAssocSemiring α]
    [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type*) : (I → α) →ₙ+* I → β :=
  { f.toMulHom.compLeft I, f.toAddMonoidHom.compLeft I with toFun := fun h => f ∘ h }

Post-composition of non-unital ring homomorphism on function spaces

Informal description

Given non-unital non-associative semirings $\alpha$ and $\beta$, and a non-unital ring homomorphism $f \colon \alpha \to \beta$, the function `NonUnitalRingHom.compLeft` constructs a non-unital ring homomorphism from the function space $I \to \alpha$ to $I \to \beta$ by post-composing with $f$. Explicitly, it maps a function $h \colon I \to \alpha$ to the composition $f \circ h \colon I \to \beta$. This homomorphism preserves both the additive and multiplicative structures pointwise.

Pi.evalRingHom definition

(f : I → Type v) [∀ i, NonAssocSemiring (f i)] (i : I) : (∀ i, f i) →+* f i

Full source

/-- Evaluation of functions into an indexed collection of rings at a point is a ring
homomorphism. This is `Function.eval` as a `RingHom`. -/
@[simps!]
def Pi.evalRingHom (f : I → Type v) [∀ i, NonAssocSemiring (f i)] (i : I) : (∀ i, f i) →+* f i :=
  { Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }

Evaluation ring homomorphism for product of semirings

Informal description

For an indexed family of non-associative semirings $(f_i)_{i \in I}$, the evaluation map at index $i$ is a ring homomorphism from the product semiring $\prod_{i \in I} f_i$ to $f_i$. Specifically, it maps a function $g$ in the product to its value $g(i)$ at index $i$, preserving both the additive and multiplicative structures, including the zero and one elements.

instRingHomSurjectiveForallEvalRingHom instance

(f : I → Type*) [∀ i, Semiring (f i)] (i) : RingHomSurjective (Pi.evalRingHom f i)

Full source

instance (f : I → Type*) [∀ i, Semiring (f i)] (i) :
    RingHomSurjective (Pi.evalRingHom f i) where
  is_surjective x := ⟨by classical exact (if h : · = i then h ▸ x else 0), by simp⟩

Surjectivity of Evaluation Ring Homomorphisms on Product Semirings

Informal description

For any indexed family of semirings $(f_i)_{i \in I}$, the evaluation ring homomorphism $\pi_i \colon \prod_{i \in I} f_i \to f_i$ is surjective for each $i \in I$.

Pi.constRingHom definition

(α β : Type*) [NonAssocSemiring β] : β →+* α → β

Full source

/-- `Function.const` as a `RingHom`. -/
@[simps]
def Pi.constRingHom (α β : Type*) [NonAssocSemiring β] : β →+* α → β :=
  { Pi.ringHom fun _ => RingHom.id β with toFun := Function.const _ }

Constant function as a ring homomorphism

Informal description

The function `Pi.constRingHom` maps an element $b$ of a non-associative semiring $\beta$ to the constant function $\alpha \to \beta$ that returns $b$ for every input. This forms a ring homomorphism from $\beta$ to the function space $\alpha \to \beta$ with pointwise operations.

RingHom.compLeft definition

{α β : Type*} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type*) : (I → α) →+* I → β

Full source

/-- Ring homomorphism between the function spaces `I → α` and `I → β`, induced by a ring
homomorphism `f` between `α` and `β`. -/
@[simps]
protected def RingHom.compLeft {α β : Type*} [NonAssocSemiring α] [NonAssocSemiring β]
    (f : α →+* β) (I : Type*) : (I → α) →+* I → β :=
  { f.toMonoidHom.compLeft I, f.toAddMonoidHom.compLeft I with toFun := fun h => f ∘ h }

Post-composition (semi-)ring homomorphism on function spaces

Informal description

Given a (semi-)ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, and a type $I$, the function `RingHom.compLeft` constructs a (semi-)ring homomorphism from the function space $I \to \alpha$ to $I \to \beta$ by post-composing with $f$. Specifically, it maps any function $h \colon I \to \alpha$ to the composition $f \circ h \colon I \to \beta$.