Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot

! This file was ported from Lean 3 source module algebra.ring.pi
! leanprover-community/mathlib commit ba2245edf0c8bb155f1569fd9b9492a9b384cde6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Pi
import Mathlib.Algebra.Hom.Ring

/-!
# Pi instances for ring

This file defines instances for ring, semiring and related structures on Pi Types
-/

-- Porting notes: used to import `tactic.pi_instances`

namespace Pi

universe u v w

variable {
I: Type u
I : 
Type u: Type (u+1)
Type u}

-- The indexing type
variable {
f: I β†’ Type v
f : 
I: Type u
I β†’ 
Type v: Type (v+1)
Type v}

-- The family of types already equipped with instances
variable (
x: (i : I) β†’ f i
x 
y: (i : I) β†’ f i
y : βˆ€ 
i: ?m.23
i, 
f: I β†’ Type v
f 
i: ?m.23
i) (
i: I
i : 
I: Type u
I)

-- Porting note: All these instances used `refine_struct` and `pi_instance_derive_field`

instance 
distrib: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Distrib (f i)] β†’ Distrib ((i : I) β†’ f i)
distrib [βˆ€ 
i: ?m.51
i, 
Distrib: Type ?u.54 β†’ Type ?u.54
Distrib <| 
f: I β†’ Type v
f 
i: ?m.51
i] : 
Distrib: Type ?u.58 β†’ Type ?u.58
Distrib (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  { add := 
(Β· + Β·): ((i : I) β†’ f i) β†’ ((i : I) β†’ f i) β†’ (i : I) β†’ f i
(Β· + Β·)
    mul := 
(Β· * Β·): ((i : I) β†’ f i) β†’ ((i : I) β†’ f i) β†’ (i : I) β†’ f i
(Β· * Β·)
    left_distrib := 
Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), a * (b + c) = a * b + a * c
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), a * (b + c) = a * b + a * c
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

x✝: I

h
(a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

x✝: I

h
(a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), a * (b + c) = a * b + a * c
Goals accomplished! πŸ™

    right_distrib := 
Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), (a + b) * c = a * c + b * c
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

(a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

(a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), (a + b) * c = a * c + b * c
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

x✝: I

h
((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

a✝, b✝, c✝: (i : I) β†’ f i

x✝: I

h
((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

inst✝: (i : I) β†’ Distrib (f i)

βˆ€ (a b c : (i : I) β†’ f i), (a + b) * c = a * c + b * c
Goals accomplished! πŸ™
}
#align pi.distrib 
Pi.distrib: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Distrib (f i)] β†’ Distrib ((i : I) β†’ f i)
Pi.distrib

instance 
nonUnitalNonAssocSemiring: {I : Type u} β†’
  {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ NonUnitalNonAssocSemiring ((i : I) β†’ f i)
nonUnitalNonAssocSemiring [βˆ€ 
i: ?m.1426
i, 
NonUnitalNonAssocSemiring: Type ?u.1429 β†’ Type ?u.1429
NonUnitalNonAssocSemiring <| 
f: I β†’ Type v
f 
i: ?m.1426
i] :
    
NonUnitalNonAssocSemiring: Type ?u.1433 β†’ Type ?u.1433
NonUnitalNonAssocSemiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
{ 
Pi.distrib: {I : Type ?u.1444} β†’ {f : I β†’ Type ?u.1443} β†’ [inst : (i : I) β†’ Distrib (f i)] β†’ Distrib ((i : I) β†’ f i)
Pi.distrib
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
, 
Pi.addCommMonoid: {I : Type ?u.1475} β†’ {f : I β†’ Type ?u.1474} β†’ [inst : (i : I) β†’ AddCommMonoid (f i)] β†’ AddCommMonoid ((i : I) β†’ f i)
Pi.addCommMonoid
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
, 
Pi.mulZeroClass: {I : Type ?u.1524} β†’ {f : I β†’ Type ?u.1523} β†’ [inst : (i : I) β†’ MulZeroClass (f i)] β†’ MulZeroClass ((i : I) β†’ f i)
Pi.mulZeroClass
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
 
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
with
{ Pi.distrib, Pi.addCommMonoid, Pi.mulZeroClass with }: NonUnitalNonAssocSemiring ?m.1557
 }
#align pi.non_unital_non_assoc_semiring 
Pi.nonUnitalNonAssocSemiring: {I : Type u} β†’
  {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ NonUnitalNonAssocSemiring ((i : I) β†’ f i)
Pi.nonUnitalNonAssocSemiring

instance 
nonUnitalSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ NonUnitalSemiring ((i : I) β†’ f i)
nonUnitalSemiring [βˆ€ 
i: ?m.1982
i, 
NonUnitalSemiring: Type ?u.1985 β†’ Type ?u.1985
NonUnitalSemiring <| 
f: I β†’ Type v
f 
i: ?m.1982
i] : 
NonUnitalSemiring: Type ?u.1989 β†’ Type ?u.1989
NonUnitalSemiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }: NonUnitalSemiring ?m.2066
{ 
Pi.nonUnitalNonAssocSemiring: {I : Type ?u.2000} β†’
  {f : I β†’ Type ?u.1999} β†’
    [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ NonUnitalNonAssocSemiring ((i : I) β†’ f i)
Pi.nonUnitalNonAssocSemiring
{ Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }: NonUnitalSemiring ?m.2066
, 
Pi.semigroupWithZero: {I : Type ?u.2035} β†’
  {f : I β†’ Type ?u.2034} β†’ [inst : (i : I) β†’ SemigroupWithZero (f i)] β†’ SemigroupWithZero ((i : I) β†’ f i)
Pi.semigroupWithZero
{ Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }: NonUnitalSemiring ?m.2066
 
{ Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }: NonUnitalSemiring ?m.2066
with
{ Pi.nonUnitalNonAssocSemiring, Pi.semigroupWithZero with }: NonUnitalSemiring ?m.2066
 }
#align pi.non_unital_semiring 
Pi.nonUnitalSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ NonUnitalSemiring ((i : I) β†’ f i)
Pi.nonUnitalSemiring

instance 
nonAssocSemiring: [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ NonAssocSemiring ((i : I) β†’ f i)
nonAssocSemiring [βˆ€ 
i: ?m.2495
i, 
NonAssocSemiring: Type ?u.2498 β†’ Type ?u.2498
NonAssocSemiring <| 
f: I β†’ Type v
f 
i: ?m.2495
i] : 
NonAssocSemiring: Type ?u.2502 β†’ Type ?u.2502
NonAssocSemiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
{ 
Pi.nonUnitalNonAssocSemiring: {I : Type ?u.2513} β†’
  {f : I β†’ Type ?u.2512} β†’
    [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ NonUnitalNonAssocSemiring ((i : I) β†’ f i)
Pi.nonUnitalNonAssocSemiring
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
, 
Pi.mulZeroOneClass: {I : Type ?u.2548} β†’ {f : I β†’ Type ?u.2547} β†’ [inst : (i : I) β†’ MulZeroOneClass (f i)] β†’ MulZeroOneClass ((i : I) β†’ f i)
Pi.mulZeroOneClass
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
, 
Pi.addMonoidWithOne: {I : Type ?u.2581} β†’
  {f : I β†’ Type ?u.2580} β†’ [inst : (i : I) β†’ AddMonoidWithOne (f i)] β†’ AddMonoidWithOne ((i : I) β†’ f i)
Pi.addMonoidWithOne
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
 
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
with
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }: NonAssocSemiring ?m.2612
 }
#align pi.non_assoc_semiring 
Pi.nonAssocSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ NonAssocSemiring ((i : I) β†’ f i)
Pi.nonAssocSemiring

instance 
semiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Semiring (f i)] β†’ Semiring ((i : I) β†’ f i)
semiring [βˆ€ 
i: ?m.3283
i, 
Semiring: Type ?u.3286 β†’ Type ?u.3286
Semiring <| 
f: I β†’ Type v
f 
i: ?m.3283
i] : 
Semiring: Type ?u.3290 β†’ Type ?u.3290
Semiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
{ 
Pi.nonUnitalSemiring: {I : Type ?u.3301} β†’
  {f : I β†’ Type ?u.3300} β†’ [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ NonUnitalSemiring ((i : I) β†’ f i)
Pi.nonUnitalSemiring
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
, 
Pi.nonAssocSemiring: {I : Type ?u.3336} β†’
  {f : I β†’ Type ?u.3335} β†’ [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ NonAssocSemiring ((i : I) β†’ f i)
Pi.nonAssocSemiring
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
, 
Pi.monoidWithZero: {I : Type ?u.3369} β†’ {f : I β†’ Type ?u.3368} β†’ [inst : (i : I) β†’ MonoidWithZero (f i)] β†’ MonoidWithZero ((i : I) β†’ f i)
Pi.monoidWithZero
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
 
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
with
{ Pi.nonUnitalSemiring, Pi.nonAssocSemiring, Pi.monoidWithZero with }: Semiring ?m.3404
 }
#align pi.semiring 
Pi.semiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Semiring (f i)] β†’ Semiring ((i : I) β†’ f i)
Pi.semiring

instance 
nonUnitalCommSemiring: [inst : (i : I) β†’ NonUnitalCommSemiring (f i)] β†’ NonUnitalCommSemiring ((i : I) β†’ f i)
nonUnitalCommSemiring [βˆ€ 
i: ?m.4086
i, 
NonUnitalCommSemiring: Type ?u.4089 β†’ Type ?u.4089
NonUnitalCommSemiring <| 
f: I β†’ Type v
f 
i: ?m.4086
i] :
    
NonUnitalCommSemiring: Type ?u.4093 β†’ Type ?u.4093
NonUnitalCommSemiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalSemiring, Pi.commSemigroup with }: NonUnitalCommSemiring ?m.4172
{ 
Pi.nonUnitalSemiring: {I : Type ?u.4104} β†’
  {f : I β†’ Type ?u.4103} β†’ [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ NonUnitalSemiring ((i : I) β†’ f i)
Pi.nonUnitalSemiring
{ Pi.nonUnitalSemiring, Pi.commSemigroup with }: NonUnitalCommSemiring ?m.4172
, 
Pi.commSemigroup: {I : Type ?u.4139} β†’ {f : I β†’ Type ?u.4138} β†’ [inst : (i : I) β†’ CommSemigroup (f i)] β†’ CommSemigroup ((i : I) β†’ f i)
Pi.commSemigroup
{ Pi.nonUnitalSemiring, Pi.commSemigroup with }: NonUnitalCommSemiring ?m.4172
 
{ Pi.nonUnitalSemiring, Pi.commSemigroup with }: NonUnitalCommSemiring ?m.4172
with
{ Pi.nonUnitalSemiring, Pi.commSemigroup with }: NonUnitalCommSemiring ?m.4172
 }
#align pi.non_unital_comm_semiring 
Pi.nonUnitalCommSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalCommSemiring (f i)] β†’ NonUnitalCommSemiring ((i : I) β†’ f i)
Pi.nonUnitalCommSemiring

instance 
commSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ CommSemiring (f i)] β†’ CommSemiring ((i : I) β†’ f i)
commSemiring [βˆ€ 
i: ?m.4454
i, 
CommSemiring: Type ?u.4457 β†’ Type ?u.4457
CommSemiring <| 
f: I β†’ Type v
f 
i: ?m.4454
i] : 
CommSemiring: Type ?u.4461 β†’ Type ?u.4461
CommSemiring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.semiring, Pi.commMonoid with }: CommSemiring ?m.4550
{ 
Pi.semiring: {I : Type ?u.4472} β†’ {f : I β†’ Type ?u.4471} β†’ [inst : (i : I) β†’ Semiring (f i)] β†’ Semiring ((i : I) β†’ f i)
Pi.semiring
{ Pi.semiring, Pi.commMonoid with }: CommSemiring ?m.4550
, 
Pi.commMonoid: {I : Type ?u.4507} β†’ {f : I β†’ Type ?u.4506} β†’ [inst : (i : I) β†’ CommMonoid (f i)] β†’ CommMonoid ((i : I) β†’ f i)
Pi.commMonoid
{ Pi.semiring, Pi.commMonoid with }: CommSemiring ?m.4550
 
{ Pi.semiring, Pi.commMonoid with }: CommSemiring ?m.4550
with
{ Pi.semiring, Pi.commMonoid with }: CommSemiring ?m.4550
 }
#align pi.comm_semiring 
Pi.commSemiring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ CommSemiring (f i)] β†’ CommSemiring ((i : I) β†’ f i)
Pi.commSemiring

instance 
nonUnitalNonAssocRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalNonAssocRing (f i)] β†’ NonUnitalNonAssocRing ((i : I) β†’ f i)
nonUnitalNonAssocRing [βˆ€ 
i: ?m.4896
i, 
NonUnitalNonAssocRing: Type ?u.4899 β†’ Type ?u.4899
NonUnitalNonAssocRing <| 
f: I β†’ Type v
f 
i: ?m.4896
i] :
    
NonUnitalNonAssocRing: Type ?u.4903 β†’ Type ?u.4903
NonUnitalNonAssocRing (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }: NonUnitalNonAssocRing ?m.4990
{ 
Pi.addCommGroup: {I : Type ?u.4914} β†’ {f : I β†’ Type ?u.4913} β†’ [inst : (i : I) β†’ AddCommGroup (f i)] β†’ AddCommGroup ((i : I) β†’ f i)
Pi.addCommGroup
{ Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }: NonUnitalNonAssocRing ?m.4990
, 
Pi.nonUnitalNonAssocSemiring: {I : Type ?u.4957} β†’
  {f : I β†’ Type ?u.4956} β†’
    [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ NonUnitalNonAssocSemiring ((i : I) β†’ f i)
Pi.nonUnitalNonAssocSemiring
{ Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }: NonUnitalNonAssocRing ?m.4990
 
{ Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }: NonUnitalNonAssocRing ?m.4990
with
{ Pi.addCommGroup, Pi.nonUnitalNonAssocSemiring with }: NonUnitalNonAssocRing ?m.4990
 }
#align pi.non_unital_non_assoc_ring 
Pi.nonUnitalNonAssocRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalNonAssocRing (f i)] β†’ NonUnitalNonAssocRing ((i : I) β†’ f i)
Pi.nonUnitalNonAssocRing

instance 
nonUnitalRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalRing (f i)] β†’ NonUnitalRing ((i : I) β†’ f i)
nonUnitalRing [βˆ€ 
i: ?m.5363
i, 
NonUnitalRing: Type ?u.5366 β†’ Type ?u.5366
NonUnitalRing <| 
f: I β†’ Type v
f 
i: ?m.5363
i] : 
NonUnitalRing: Type ?u.5370 β†’ Type ?u.5370
NonUnitalRing (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }: NonUnitalRing ?m.5447
{ 
Pi.nonUnitalNonAssocRing: {I : Type ?u.5381} β†’
  {f : I β†’ Type ?u.5380} β†’ [inst : (i : I) β†’ NonUnitalNonAssocRing (f i)] β†’ NonUnitalNonAssocRing ((i : I) β†’ f i)
Pi.nonUnitalNonAssocRing
{ Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }: NonUnitalRing ?m.5447
, 
Pi.nonUnitalSemiring: {I : Type ?u.5414} β†’
  {f : I β†’ Type ?u.5413} β†’ [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ NonUnitalSemiring ((i : I) β†’ f i)
Pi.nonUnitalSemiring
{ Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }: NonUnitalRing ?m.5447
 
{ Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }: NonUnitalRing ?m.5447
with
{ Pi.nonUnitalNonAssocRing, Pi.nonUnitalSemiring with }: NonUnitalRing ?m.5447
 }
#align pi.non_unital_ring 
Pi.nonUnitalRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalRing (f i)] β†’ NonUnitalRing ((i : I) β†’ f i)
Pi.nonUnitalRing

instance 
nonAssocRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonAssocRing (f i)] β†’ NonAssocRing ((i : I) β†’ f i)
nonAssocRing [βˆ€ 
i: ?m.5858
i, 
NonAssocRing: Type ?u.5861 β†’ Type ?u.5861
NonAssocRing <| 
f: I β†’ Type v
f 
i: ?m.5858
i] : 
NonAssocRing: Type ?u.5865 β†’ Type ?u.5865
NonAssocRing (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
{ 
Pi.nonUnitalNonAssocRing: {I : Type ?u.5876} β†’
  {f : I β†’ Type ?u.5875} β†’ [inst : (i : I) β†’ NonUnitalNonAssocRing (f i)] β†’ NonUnitalNonAssocRing ((i : I) β†’ f i)
Pi.nonUnitalNonAssocRing
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
, 
Pi.nonAssocSemiring: {I : Type ?u.5909} β†’
  {f : I β†’ Type ?u.5908} β†’ [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ NonAssocSemiring ((i : I) β†’ f i)
Pi.nonAssocSemiring
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
, 
Pi.addGroupWithOne: {I : Type ?u.5942} β†’ {f : I β†’ Type ?u.5941} β†’ [inst : (i : I) β†’ AddGroupWithOne (f i)] β†’ AddGroupWithOne ((i : I) β†’ f i)
Pi.addGroupWithOne
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
 
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
with
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }: NonAssocRing ?m.5973
 }
#align pi.non_assoc_ring 
Pi.nonAssocRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonAssocRing (f i)] β†’ NonAssocRing ((i : I) β†’ f i)
Pi.nonAssocRing

instance 
ring: [inst : (i : I) β†’ Ring (f i)] β†’ Ring ((i : I) β†’ f i)
ring [βˆ€ 
i: ?m.6717
i, 
Ring: Type ?u.6720 β†’ Type ?u.6720
Ring <| 
f: I β†’ Type v
f 
i: ?m.6717
i] : 
Ring: Type ?u.6724 β†’ Type ?u.6724
Ring (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
{ 
Pi.semiring: {I : Type ?u.6735} β†’ {f : I β†’ Type ?u.6734} β†’ [inst : (i : I) β†’ Semiring (f i)] β†’ Semiring ((i : I) β†’ f i)
Pi.semiring
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
, 
Pi.addCommGroup: {I : Type ?u.6770} β†’ {f : I β†’ Type ?u.6769} β†’ [inst : (i : I) β†’ AddCommGroup (f i)] β†’ AddCommGroup ((i : I) β†’ f i)
Pi.addCommGroup
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
, 
Pi.addGroupWithOne: {I : Type ?u.6813} β†’ {f : I β†’ Type ?u.6812} β†’ [inst : (i : I) β†’ AddGroupWithOne (f i)] β†’ AddGroupWithOne ((i : I) β†’ f i)
Pi.addGroupWithOne
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
 
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
with
{ Pi.semiring, Pi.addCommGroup, Pi.addGroupWithOne with }: Ring ?m.6844
 }
#align pi.ring 
Pi.ring: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Ring (f i)] β†’ Ring ((i : I) β†’ f i)
Pi.ring

instance 
nonUnitalCommRing: [inst : (i : I) β†’ NonUnitalCommRing (f i)] β†’ NonUnitalCommRing ((i : I) β†’ f i)
nonUnitalCommRing [βˆ€ 
i: ?m.7696
i, 
NonUnitalCommRing: Type ?u.7699 β†’ Type ?u.7699
NonUnitalCommRing <| 
f: I β†’ Type v
f 
i: ?m.7696
i] : 
NonUnitalCommRing: Type ?u.7703 β†’ Type ?u.7703
NonUnitalCommRing (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.nonUnitalRing, Pi.commSemigroup with }: NonUnitalCommRing ?m.7780
{ 
Pi.nonUnitalRing: {I : Type ?u.7714} β†’ {f : I β†’ Type ?u.7713} β†’ [inst : (i : I) β†’ NonUnitalRing (f i)] β†’ NonUnitalRing ((i : I) β†’ f i)
Pi.nonUnitalRing
{ Pi.nonUnitalRing, Pi.commSemigroup with }: NonUnitalCommRing ?m.7780
, 
Pi.commSemigroup: {I : Type ?u.7747} β†’ {f : I β†’ Type ?u.7746} β†’ [inst : (i : I) β†’ CommSemigroup (f i)] β†’ CommSemigroup ((i : I) β†’ f i)
Pi.commSemigroup
{ Pi.nonUnitalRing, Pi.commSemigroup with }: NonUnitalCommRing ?m.7780
 
{ Pi.nonUnitalRing, Pi.commSemigroup with }: NonUnitalCommRing ?m.7780
with
{ Pi.nonUnitalRing, Pi.commSemigroup with }: NonUnitalCommRing ?m.7780
 }
#align pi.non_unital_comm_ring 
Pi.nonUnitalCommRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ NonUnitalCommRing (f i)] β†’ NonUnitalCommRing ((i : I) β†’ f i)
Pi.nonUnitalCommRing

instance 
commRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ CommRing (f i)] β†’ CommRing ((i : I) β†’ f i)
commRing [βˆ€ 
i: ?m.8044
i, 
CommRing: Type ?u.8047 β†’ Type ?u.8047
CommRing <| 
f: I β†’ Type v
f 
i: ?m.8044
i] : 
CommRing: Type ?u.8051 β†’ Type ?u.8051
CommRing (βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) :=
  
{ Pi.ring, Pi.commSemiring with }: CommRing ?m.8122
{ 
Pi.ring: {I : Type ?u.8062} β†’ {f : I β†’ Type ?u.8061} β†’ [inst : (i : I) β†’ Ring (f i)] β†’ Ring ((i : I) β†’ f i)
Pi.ring
{ Pi.ring, Pi.commSemiring with }: CommRing ?m.8122
, 
Pi.commSemiring: {I : Type ?u.8093} β†’ {f : I β†’ Type ?u.8092} β†’ [inst : (i : I) β†’ CommSemiring (f i)] β†’ CommSemiring ((i : I) β†’ f i)
Pi.commSemiring
{ Pi.ring, Pi.commSemiring with }: CommRing ?m.8122
 
{ Pi.ring, Pi.commSemiring with }: CommRing ?m.8122
with
{ Pi.ring, Pi.commSemiring with }: CommRing ?m.8122
 }
#align pi.comm_ring 
Pi.commRing: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ CommRing (f i)] β†’ CommRing ((i : I) β†’ f i)
Pi.commRing

/-- 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: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring Ξ³] (g : (i : I) β†’ Ξ³ β†’β‚™+* f i) (x : Ξ³) (b : I),
  ↑(Pi.nonUnitalRingHom g) x b = ↑(g b) x
simps]
protected def 
nonUnitalRingHom: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    {Ξ³ : Type w} β†’
      [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’
        [inst_1 : NonUnitalNonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’β‚™+* f i) β†’ Ξ³ β†’β‚™+* (i : I) β†’ f i
nonUnitalRingHom {
Ξ³: Type w
Ξ³ : 
Type w: Type (w+1)
Type w} [βˆ€ 
i: ?m.8497
i, 
NonUnitalNonAssocSemiring: Type ?u.8500 β†’ Type ?u.8500
NonUnitalNonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.8497
i)]
    [
NonUnitalNonAssocSemiring: Type ?u.8504 β†’ Type ?u.8504
NonUnitalNonAssocSemiring 
Ξ³: Type w
Ξ³] (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g : βˆ€ 
i: ?m.8508
i, 
Ξ³: Type w
Ξ³ β†’β‚™+* 
f: I β†’ Type v
f 
i: ?m.8508
i) : 
Ξ³: Type w
Ξ³ β†’β‚™+* βˆ€ 
i: ?m.8536
i, 
f: I β†’ Type v
f 
i: ?m.8536
i :=
  { 
Pi.mulHom: {I : Type ?u.8586} β†’
  {f : I β†’ Type ?u.8585} β†’
    {Ξ³ : Type ?u.8584} β†’ [inst : (i : I) β†’ Mul (f i)] β†’ [inst_1 : Mul Ξ³] β†’ ((i : I) β†’ Ξ³ β†’β‚™* f i) β†’ Ξ³ β†’β‚™* (i : I) β†’ f i
Pi.mulHom fun 
i: ?m.8635
i => (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g 
i: ?m.8635
i).
toMulHom: {Ξ± : Type ?u.8638} β†’
  {Ξ² : Type ?u.8637} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’ [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ Ξ± β†’β‚™* Ξ²
toMulHom, 
Pi.addMonoidHom: {I : Type ?u.8827} β†’
  {f : I β†’ Type ?u.8826} β†’
    {Ξ³ : Type ?u.8825} β†’
      [inst : (i : I) β†’ AddZeroClass (f i)] β†’ [inst_1 : AddZeroClass Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+ f i) β†’ Ξ³ β†’+ (i : I) β†’ f i
Pi.addMonoidHom fun 
i: ?m.8856
i => (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g 
i: ?m.8856
i).
toAddMonoidHom: {Ξ± : Type ?u.8859} β†’
  {Ξ² : Type ?u.8858} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’ [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ Ξ± β†’+ Ξ²
toAddMonoidHom with
    toFun := fun 
x: ?m.9652
x 
b: ?m.9655
b => 
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g 
b: ?m.9655
b 
x: ?m.9652
x }
#align pi.non_unital_ring_hom 
Pi.nonUnitalRingHom: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    {Ξ³ : Type w} β†’
      [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’
        [inst_1 : NonUnitalNonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’β‚™+* f i) β†’ Ξ³ β†’β‚™+* (i : I) β†’ f i
Pi.nonUnitalRingHom

theorem 
nonUnitalRingHom_injective: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : Nonempty I] [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring Ξ³] (g : (i : I) β†’ Ξ³ β†’β‚™+* f i),
  (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(Pi.nonUnitalRingHom g)
nonUnitalRingHom_injective {
Ξ³: Type w
Ξ³ : 
Type w: Type (w+1)
Type w} [
Nonempty: Sort ?u.11106 β†’ Prop
Nonempty 
I: Type u
I]
    [βˆ€ 
i: ?m.11110
i, 
NonUnitalNonAssocSemiring: Type ?u.11113 β†’ Type ?u.11113
NonUnitalNonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.11110
i)] [
NonUnitalNonAssocSemiring: Type ?u.11117 β†’ Type ?u.11117
NonUnitalNonAssocSemiring 
Ξ³: Type w
Ξ³] (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g : βˆ€ 
i: ?m.11121
i, 
Ξ³: Type w
Ξ³ β†’β‚™+* 
f: I β†’ Type v
f 
i: ?m.11121
i)
    (
hg: βˆ€ (i : I), Function.Injective ↑(g i)
hg : βˆ€ 
i: ?m.11147
i, 
Function.Injective: {Ξ± : Sort ?u.11151} β†’ {Ξ² : Sort ?u.11150} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g 
i: ?m.11147
i)) : 
Function.Injective: {Ξ± : Sort ?u.11358} β†’ {Ξ² : Sort ?u.11357} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
Pi.nonUnitalRingHom: {I : Type ?u.11363} β†’
  {f : I β†’ Type ?u.11362} β†’
    {Ξ³ : Type ?u.11361} β†’
      [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’
        [inst_1 : NonUnitalNonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’β‚™+* f i) β†’ Ξ³ β†’β‚™+* (i : I) β†’ f i
Pi.nonUnitalRingHom 
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g) :=
  
mulHom_injective: βˆ€ {I : Type ?u.11644} {f : I β†’ Type ?u.11643} {Ξ³ : Type ?u.11642} [inst : Nonempty I] [inst : (i : I) β†’ Mul (f i)]
  [inst_1 : Mul Ξ³] (g : (i : I) β†’ Ξ³ β†’β‚™* f i), (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(mulHom g)
mulHom_injective (fun 
i: ?m.11652
i => (
g: (i : I) β†’ Ξ³ β†’β‚™+* f i
g 
i: ?m.11652
i).
toMulHom: {Ξ± : Type ?u.11655} β†’
  {Ξ² : Type ?u.11654} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’ [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ Ξ± β†’β‚™* Ξ²
toMulHom) 
hg: βˆ€ (i : I), Function.Injective ↑(g i)
hg
#align pi.non_unital_ring_hom_injective 
Pi.nonUnitalRingHom_injective: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : Nonempty I] [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring Ξ³] (g : (i : I) β†’ Ξ³ β†’β‚™+* f i),
  (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(Pi.nonUnitalRingHom g)
Pi.nonUnitalRingHom_injective

/-- 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: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : (i : I) β†’ NonAssocSemiring (f i)] [inst_1 : NonAssocSemiring Ξ³]
  (g : (i : I) β†’ Ξ³ β†’+* f i) (x : Ξ³) (b : I), ↑(Pi.ringHom g) x b = ↑(g b) x
simps]
protected def 
ringHom: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    {Ξ³ : Type w} β†’
      [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’
        [inst_1 : NonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+* f i) β†’ Ξ³ β†’+* (i : I) β†’ f i
ringHom {
Ξ³: Type w
Ξ³ : 
Type w: Type (w+1)
Type w} [βˆ€ 
i: ?m.11911
i, 
NonAssocSemiring: Type ?u.11914 β†’ Type ?u.11914
NonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.11911
i)] [
NonAssocSemiring: Type ?u.11918 β†’ Type ?u.11918
NonAssocSemiring 
Ξ³: Type w
Ξ³]
    (
g: (i : I) β†’ Ξ³ β†’+* f i
g : βˆ€ 
i: ?m.11922
i, 
Ξ³: Type w
Ξ³ β†’+* 
f: I β†’ Type v
f 
i: ?m.11922
i) : 
Ξ³: Type w
Ξ³ β†’+* βˆ€ 
i: ?m.11948
i, 
f: I β†’ Type v
f 
i: ?m.11948
i :=
  { 
Pi.monoidHom: {I : Type ?u.11996} β†’
  {f : I β†’ Type ?u.11995} β†’
    {Ξ³ : Type ?u.11994} β†’
      [inst : (i : I) β†’ MulOneClass (f i)] β†’ [inst_1 : MulOneClass Ξ³] β†’ ((i : I) β†’ Ξ³ β†’* f i) β†’ Ξ³ β†’* (i : I) β†’ f i
Pi.monoidHom fun 
i: ?m.12027
i => (
g: (i : I) β†’ Ξ³ β†’+* f i
g 
i: ?m.12027
i).
toMonoidHom: {Ξ± : Type ?u.12030} β†’
  {Ξ² : Type ?u.12029} β†’ [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ Ξ± β†’* Ξ²
toMonoidHom, 
Pi.addMonoidHom: {I : Type ?u.12122} β†’
  {f : I β†’ Type ?u.12121} β†’
    {Ξ³ : Type ?u.12120} β†’
      [inst : (i : I) β†’ AddZeroClass (f i)] β†’ [inst_1 : AddZeroClass Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+ f i) β†’ Ξ³ β†’+ (i : I) β†’ f i
Pi.addMonoidHom fun 
i: ?m.12151
i => (
g: (i : I) β†’ Ξ³ β†’+* f i
g 
i: ?m.12151
i).
toAddMonoidHom: {Ξ± : Type ?u.12154} β†’
  {Ξ² : Type ?u.12153} β†’ [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ Ξ± β†’+ Ξ²
toAddMonoidHom with
    toFun := fun 
x: ?m.12660
x 
b: ?m.12663
b => 
g: (i : I) β†’ Ξ³ β†’+* f i
g 
b: ?m.12663
b 
x: ?m.12660
x }
#align pi.ring_hom 
Pi.ringHom: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    {Ξ³ : Type w} β†’
      [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’
        [inst_1 : NonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+* f i) β†’ Ξ³ β†’+* (i : I) β†’ f i
Pi.ringHom
#align pi.ring_hom_apply 
Pi.ringHom_apply: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : (i : I) β†’ NonAssocSemiring (f i)] [inst_1 : NonAssocSemiring Ξ³]
  (g : (i : I) β†’ Ξ³ β†’+* f i) (x : Ξ³) (b : I), ↑(Pi.ringHom g) x b = ↑(g b) x
Pi.ringHom_apply

theorem 
ringHom_injective: βˆ€ {Ξ³ : Type w} [inst : Nonempty I] [inst : (i : I) β†’ NonAssocSemiring (f i)] [inst_1 : NonAssocSemiring Ξ³]
  (g : (i : I) β†’ Ξ³ β†’+* f i), (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(Pi.ringHom g)
ringHom_injective {
Ξ³: Type w
Ξ³ : 
Type w: Type (w+1)
Type w} [
Nonempty: Sort ?u.13733 β†’ Prop
Nonempty 
I: Type u
I] [βˆ€ 
i: ?m.13737
i, 
NonAssocSemiring: Type ?u.13740 β†’ Type ?u.13740
NonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.13737
i)]
    [
NonAssocSemiring: Type ?u.13744 β†’ Type ?u.13744
NonAssocSemiring 
Ξ³: Type w
Ξ³] (
g: (i : I) β†’ Ξ³ β†’+* f i
g : βˆ€ 
i: ?m.13748
i, 
Ξ³: Type w
Ξ³ β†’+* 
f: I β†’ Type v
f 
i: ?m.13748
i) (
hg: βˆ€ (i : I), Function.Injective ↑(g i)
hg : βˆ€ 
i: ?m.13772
i, 
Function.Injective: {Ξ± : Sort ?u.13776} β†’ {Ξ² : Sort ?u.13775} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
g: (i : I) β†’ Ξ³ β†’+* f i
g 
i: ?m.13772
i)) :
    
Function.Injective: {Ξ± : Sort ?u.14042} β†’ {Ξ² : Sort ?u.14041} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
Pi.ringHom: {I : Type ?u.14047} β†’
  {f : I β†’ Type ?u.14046} β†’
    {Ξ³ : Type ?u.14045} β†’
      [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’
        [inst_1 : NonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+* f i) β†’ Ξ³ β†’+* (i : I) β†’ f i
Pi.ringHom 
g: (i : I) β†’ Ξ³ β†’+* f i
g) :=
  
monoidHom_injective: βˆ€ {I : Type ?u.14383} {f : I β†’ Type ?u.14382} {Ξ³ : Type ?u.14381} [inst : Nonempty I]
  [inst : (i : I) β†’ MulOneClass (f i)] [inst_1 : MulOneClass Ξ³] (g : (i : I) β†’ Ξ³ β†’* f i),
  (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(monoidHom g)
monoidHom_injective (fun 
i: ?m.14391
i => (
g: (i : I) β†’ Ξ³ β†’+* f i
g 
i: ?m.14391
i).
toMonoidHom: {Ξ± : Type ?u.14394} β†’
  {Ξ² : Type ?u.14393} β†’ [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ Ξ± β†’* Ξ²
toMonoidHom) 
hg: βˆ€ (i : I), Function.Injective ↑(g i)
hg
#align pi.ring_hom_injective 
Pi.ringHom_injective: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ³ : Type w} [inst : Nonempty I] [inst : (i : I) β†’ NonAssocSemiring (f i)]
  [inst_1 : NonAssocSemiring Ξ³] (g : (i : I) β†’ Ξ³ β†’+* f i),
  (βˆ€ (i : I), Function.Injective ↑(g i)) β†’ Function.Injective ↑(Pi.ringHom g)
Pi.ringHom_injective

end Pi

section NonUnitalRingHom

universe u v

variable {
I: Type u
I : 
Type u: Type (u+1)
Type u}

/-- 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: βˆ€ {I : Type u} (f : I β†’ Type v) [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] (i : I) (a : (i : I) β†’ f i),
  ↑(evalNonUnitalRingHom f i) a = MulHom.toFun (evalMulHom f i) a
simps]
def 
Pi.evalNonUnitalRingHom: {I : Type u} β†’
  (f : I β†’ Type v) β†’ [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’β‚™+* f i
Pi.evalNonUnitalRingHom (
f: I β†’ Type v
f : 
I: Type u
I β†’ 
Type v: Type (v+1)
Type v) [βˆ€ 
i: ?m.14540
i, 
NonUnitalNonAssocSemiring: Type ?u.14543 β†’ Type ?u.14543
NonUnitalNonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.14540
i)] (
i: I
i : 
I: Type u
I) :
    (βˆ€ 
i: ?m.14552
i, 
f: I β†’ Type v
f 
i: ?m.14552
i) β†’β‚™+* 
f: I β†’ Type v
f 
i: I
i :=
  
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
{ 
Pi.evalMulHom: {I : Type ?u.14608} β†’ (f : I β†’ Type ?u.14607) β†’ [inst : (i : I) β†’ Mul (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’β‚™* f i
Pi.evalMulHom
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 
f: I β†’ Type v
f
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 
i: I
i
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
, 
Pi.evalAddMonoidHom: {I : Type ?u.14725} β†’ (f : I β†’ Type ?u.14724) β†’ [inst : (i : I) β†’ AddZeroClass (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’+ f i
Pi.evalAddMonoidHom
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 
f: I β†’ Type v
f
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 
i: I
i
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
with
{ Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }: ?m.15151 β†’β‚™+* ?m.15152
 }
#align pi.eval_non_unital_ring_hom 
Pi.evalNonUnitalRingHom: {I : Type u} β†’
  (f : I β†’ Type v) β†’ [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’β‚™+* f i
Pi.evalNonUnitalRingHom

/-- `Function.const` as a `NonUnitalRingHom`. -/
@[
simps: βˆ€ (Ξ± : Type u_1) (Ξ² : Type u_2) [inst : NonUnitalNonAssocSemiring Ξ²] (a : Ξ²) (a_1 : Ξ±),
  ↑(constNonUnitalRingHom Ξ± Ξ²) a a_1 = Function.const Ξ± a a_1
simps]
def 
Pi.constNonUnitalRingHom: (Ξ± : Type u_1) β†’ (Ξ² : Type u_2) β†’ [inst : NonUnitalNonAssocSemiring Ξ²] β†’ Ξ² β†’β‚™+* Ξ± β†’ Ξ²
Pi.constNonUnitalRingHom (
Ξ±: Type ?u.16563
Ξ± 
Ξ²: Type ?u.16566
Ξ² : 
Type _: Type (?u.16566+1)
Type _) [
NonUnitalNonAssocSemiring: Type ?u.16569 β†’ Type ?u.16569
NonUnitalNonAssocSemiring 
Ξ²: Type ?u.16566
Ξ²] : 
Ξ²: Type ?u.16566
Ξ² β†’β‚™+* 
Ξ±: Type ?u.16563
Ξ± β†’ 
Ξ²: Type ?u.16566
Ξ² :=
  { 
Pi.nonUnitalRingHom: {I : Type ?u.16625} β†’
  {f : I β†’ Type ?u.16624} β†’
    {Ξ³ : Type ?u.16623} β†’
      [inst : (i : I) β†’ NonUnitalNonAssocSemiring (f i)] β†’
        [inst_1 : NonUnitalNonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’β‚™+* f i) β†’ Ξ³ β†’β‚™+* (i : I) β†’ f i
Pi.nonUnitalRingHom fun 
_: ?m.16650
_ => 
NonUnitalRingHom.id: (Ξ± : Type ?u.16652) β†’ [inst : NonUnitalNonAssocSemiring Ξ±] β†’ Ξ± β†’β‚™+* Ξ±
NonUnitalRingHom.id 
Ξ²: Type ?u.16566
Ξ² with toFun := 
Function.const: {Ξ± : Sort ?u.16871} β†’ (Ξ² : Sort ?u.16870) β†’ Ξ± β†’ Ξ² β†’ Ξ±
Function.const 
_: Sort ?u.16870
_ }
#align pi.const_non_unital_ring_hom 
Pi.constNonUnitalRingHom: (Ξ± : Type u_1) β†’ (Ξ² : Type u_2) β†’ [inst : NonUnitalNonAssocSemiring Ξ²] β†’ Ξ² β†’β‚™+* Ξ± β†’ Ξ²
Pi.constNonUnitalRingHom

/-- Non-unital ring homomorphism between the function spaces `I β†’ Ξ±` and `I β†’ Ξ²`, induced by a
non-unital ring homomorphism `f` between `Ξ±` and `Ξ²`. -/
@[
simps: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : NonUnitalNonAssocSemiring Ξ±] [inst_1 : NonUnitalNonAssocSemiring Ξ²]
  (f : Ξ± β†’β‚™+* Ξ²) (I : Type u_3) (h : I β†’ Ξ±) (a : I), ↑(NonUnitalRingHom.compLeft f I) h a = (↑f ∘ h) a
simps]
protected def 
NonUnitalRingHom.compLeft: {Ξ± : Type u_1} β†’
  {Ξ² : Type u_2} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’
      [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ (I : Type u_3) β†’ (I β†’ Ξ±) β†’β‚™+* I β†’ Ξ²
NonUnitalRingHom.compLeft {
Ξ±: Type ?u.17200
Ξ± 
Ξ²: Type ?u.17203
Ξ² : 
Type _: Type (?u.17203+1)
Type _} [
NonUnitalNonAssocSemiring: Type ?u.17206 β†’ Type ?u.17206
NonUnitalNonAssocSemiring 
Ξ±: Type ?u.17200
Ξ±]
    [
NonUnitalNonAssocSemiring: Type ?u.17209 β†’ Type ?u.17209
NonUnitalNonAssocSemiring 
Ξ²: Type ?u.17203
Ξ²] (
f: Ξ± β†’β‚™+* Ξ²
f : 
Ξ±: Type ?u.17200
Ξ± β†’β‚™+* 
Ξ²: Type ?u.17203
Ξ²) (
I: Type ?u.17230
I : 
Type _: Type (?u.17230+1)
Type _) : (
I: Type ?u.17230
I β†’ 
Ξ±: Type ?u.17200
Ξ±) β†’β‚™+* 
I: Type ?u.17230
I β†’ 
Ξ²: Type ?u.17203
Ξ² :=
  { 
f: Ξ± β†’β‚™+* Ξ²
f.
toMulHom: {Ξ± : Type ?u.17319} β†’
  {Ξ² : Type ?u.17318} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’ [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ Ξ± β†’β‚™* Ξ²
toMulHom.
compLeft: {Ξ± : Type ?u.17338} β†’
  {Ξ² : Type ?u.17337} β†’ [inst : Mul Ξ±] β†’ [inst_1 : Mul Ξ²] β†’ (Ξ± β†’β‚™* Ξ²) β†’ (I : Type ?u.17336) β†’ (I β†’ Ξ±) β†’β‚™* I β†’ Ξ²
compLeft 
I: Type ?u.17230
I, 
f: Ξ± β†’β‚™+* Ξ²
f.
toAddMonoidHom: {Ξ± : Type ?u.17455} β†’
  {Ξ² : Type ?u.17454} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’ [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ Ξ± β†’+ Ξ²
toAddMonoidHom.
compLeft: {Ξ± : Type ?u.17462} β†’
  {Ξ² : Type ?u.17461} β†’
    [inst : AddZeroClass Ξ±] β†’ [inst_1 : AddZeroClass Ξ²] β†’ (Ξ± β†’+ Ξ²) β†’ (I : Type ?u.17460) β†’ (I β†’ Ξ±) β†’+ I β†’ Ξ²
compLeft 
I: Type ?u.17230
I with toFun := fun 
h: ?m.18101
h => 
f: Ξ± β†’β‚™+* Ξ²
f ∘ 
h: ?m.18101
h }
#align non_unital_ring_hom.comp_left 
NonUnitalRingHom.compLeft: {Ξ± : Type u_1} β†’
  {Ξ² : Type u_2} β†’
    [inst : NonUnitalNonAssocSemiring Ξ±] β†’
      [inst_1 : NonUnitalNonAssocSemiring Ξ²] β†’ (Ξ± β†’β‚™+* Ξ²) β†’ (I : Type u_3) β†’ (I β†’ Ξ±) β†’β‚™+* I β†’ Ξ²
NonUnitalRingHom.compLeft

end NonUnitalRingHom

section RingHom

universe u v

variable {
I: Type u
I : 
Type u: Type (u+1)
Type u}

/-- 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: {I : Type u} β†’ (f : I β†’ Type v) β†’ [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’+* f i
Pi.evalRingHom (
f: I β†’ Type v
f : 
I: Type u
I β†’ 
Type v: Type (v+1)
Type v) [βˆ€ 
i: ?m.19437
i, 
NonAssocSemiring: Type ?u.19440 β†’ Type ?u.19440
NonAssocSemiring (
f: I β†’ Type v
f 
i: ?m.19437
i)] (
i: I
i : 
I: Type u
I) : (βˆ€ 
i: ?m.19449
i, 
f: I β†’ Type v
f 
i: ?m.19449
i) β†’+* 
f: I β†’ Type v
f 
i: I
i :=
  
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
{ 
Pi.evalMonoidHom: {I : Type ?u.19502} β†’ (f : I β†’ Type ?u.19501) β†’ [inst : (i : I) β†’ MulOneClass (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’* f i
Pi.evalMonoidHom
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 
f: I β†’ Type v
f
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 
i: I
i
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
, 
Pi.evalAddMonoidHom: {I : Type ?u.19556} β†’ (f : I β†’ Type ?u.19555) β†’ [inst : (i : I) β†’ AddZeroClass (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’+ f i
Pi.evalAddMonoidHom
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 
f: I β†’ Type v
f
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 
i: I
i
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
with
{ Pi.evalMonoidHom f i, Pi.evalAddMonoidHom f i with }: ?m.19696 β†’+* ?m.19697
 }
#align pi.eval_ring_hom 
Pi.evalRingHom: {I : Type u} β†’ (f : I β†’ Type v) β†’ [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’ (i : I) β†’ ((i : I) β†’ f i) β†’+* f i
Pi.evalRingHom
#align pi.eval_ring_hom_apply 
Pi.evalRingHom_apply: βˆ€ {I : Type u} (f : I β†’ Type v) [inst : (i : I) β†’ NonAssocSemiring (f i)] (i : I) (g : (i : I) β†’ f i),
  ↑(Pi.evalRingHom f i) g = g i
Pi.evalRingHom_apply

/-- `Function.const` as a `RingHom`. -/
@[
simps: βˆ€ (Ξ± : Type u_1) (Ξ² : Type u_2) [inst : NonAssocSemiring Ξ²] (a : Ξ²) (a_1 : Ξ±),
  ↑(constRingHom Ξ± Ξ²) a a_1 = Function.const Ξ± a a_1
simps]
def 
Pi.constRingHom: (Ξ± : Type u_1) β†’ (Ξ² : Type u_2) β†’ [inst : NonAssocSemiring Ξ²] β†’ Ξ² β†’+* Ξ± β†’ Ξ²
Pi.constRingHom (
Ξ±: Type ?u.20503
Ξ± 
Ξ²: Type ?u.20506
Ξ² : 
Type _: Type (?u.20506+1)
Type _) [
NonAssocSemiring: Type ?u.20509 β†’ Type ?u.20509
NonAssocSemiring 
Ξ²: Type ?u.20506
Ξ²] : 
Ξ²: Type ?u.20506
Ξ² β†’+* 
Ξ±: Type ?u.20503
Ξ± β†’ 
Ξ²: Type ?u.20506
Ξ² :=
  { 
Pi.ringHom: {I : Type ?u.20562} β†’
  {f : I β†’ Type ?u.20561} β†’
    {Ξ³ : Type ?u.20560} β†’
      [inst : (i : I) β†’ NonAssocSemiring (f i)] β†’
        [inst_1 : NonAssocSemiring Ξ³] β†’ ((i : I) β†’ Ξ³ β†’+* f i) β†’ Ξ³ β†’+* (i : I) β†’ f i
Pi.ringHom fun 
_: ?m.20585
_ => 
RingHom.id: (Ξ± : Type ?u.20587) β†’ [inst : NonAssocSemiring Ξ±] β†’ Ξ± β†’+* Ξ±
RingHom.id 
Ξ²: Type ?u.20506
Ξ² with toFun := 
Function.const: {Ξ± : Sort ?u.20893} β†’ (Ξ² : Sort ?u.20892) β†’ Ξ± β†’ Ξ² β†’ Ξ±
Function.const 
_: Sort ?u.20892
_ }
#align pi.const_ring_hom 
Pi.constRingHom: (Ξ± : Type u_1) β†’ (Ξ² : Type u_2) β†’ [inst : NonAssocSemiring Ξ²] β†’ Ξ² β†’+* Ξ± β†’ Ξ²
Pi.constRingHom
#align pi.const_ring_hom_apply 
Pi.constRingHom_apply: βˆ€ (Ξ± : Type u_1) (Ξ² : Type u_2) [inst : NonAssocSemiring Ξ²] (a : Ξ²) (a_1 : Ξ±),
  ↑(Pi.constRingHom Ξ± Ξ²) a a_1 = Function.const Ξ± a a_1
Pi.constRingHom_apply

/-- Ring homomorphism between the function spaces `I β†’ Ξ±` and `I β†’ Ξ²`, induced by a ring
homomorphism `f` between `Ξ±` and `Ξ²`. -/
@[
simps: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : NonAssocSemiring Ξ±] [inst_1 : NonAssocSemiring Ξ²] (f : Ξ± β†’+* Ξ²) (I : Type u_3)
  (h : I β†’ Ξ±) (a : I), ↑(RingHom.compLeft f I) h a = (↑f ∘ h) a
simps]
protected def 
RingHom.compLeft: {Ξ± : Type ?u.21381} β†’
  {Ξ² : Type ?u.21384} β†’
    [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ (I : Type ?u.21409) β†’ (I β†’ Ξ±) β†’+* I β†’ Ξ²
RingHom.compLeft {
Ξ±: Type ?u.21381
Ξ± 
Ξ²: Type ?u.21384
Ξ² : 
Type _: Type (?u.21381+1)
Type _} [
NonAssocSemiring: Type ?u.21387 β†’ Type ?u.21387
NonAssocSemiring 
Ξ±: Type ?u.21381
Ξ±] [
NonAssocSemiring: Type ?u.21390 β†’ Type ?u.21390
NonAssocSemiring 
Ξ²: Type ?u.21384
Ξ²]
    (
f: Ξ± β†’+* Ξ²
f : 
Ξ±: Type ?u.21381
Ξ± β†’+* 
Ξ²: Type ?u.21384
Ξ²) (
I: Type ?u.21409
I : 
Type _: Type (?u.21409+1)
Type _) : (
I: Type ?u.21409
I β†’ 
Ξ±: Type ?u.21381
Ξ±) β†’+* 
I: Type ?u.21409
I β†’ 
Ξ²: Type ?u.21384
Ξ² :=
  { 
f: Ξ± β†’+* Ξ²
f.
toMonoidHom: {Ξ± : Type ?u.21494} β†’
  {Ξ² : Type ?u.21493} β†’ [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ Ξ± β†’* Ξ²
toMonoidHom.
compLeft: {Ξ± : Type ?u.21511} β†’
  {Ξ² : Type ?u.21510} β†’
    [inst : MulOneClass Ξ±] β†’ [inst_1 : MulOneClass Ξ²] β†’ (Ξ± β†’* Ξ²) β†’ (I : Type ?u.21509) β†’ (I β†’ Ξ±) β†’* I β†’ Ξ²
compLeft 
I: Type ?u.21409
I, 
f: Ξ± β†’+* Ξ²
f.
toAddMonoidHom: {Ξ± : Type ?u.21564} β†’
  {Ξ² : Type ?u.21563} β†’ [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ Ξ± β†’+ Ξ²
toAddMonoidHom.
compLeft: {Ξ± : Type ?u.21571} β†’
  {Ξ² : Type ?u.21570} β†’
    [inst : AddZeroClass Ξ±] β†’ [inst_1 : AddZeroClass Ξ²] β†’ (Ξ± β†’+ Ξ²) β†’ (I : Type ?u.21569) β†’ (I β†’ Ξ±) β†’+ I β†’ Ξ²
compLeft 
I: Type ?u.21409
I with toFun := fun 
h: ?m.22100
h => 
f: Ξ± β†’+* Ξ²
f ∘ 
h: ?m.22100
h }
#align ring_hom.comp_left 
RingHom.compLeft: {Ξ± : Type u_1} β†’
  {Ξ² : Type u_2} β†’
    [inst : NonAssocSemiring Ξ±] β†’ [inst_1 : NonAssocSemiring Ξ²] β†’ (Ξ± β†’+* Ξ²) β†’ (I : Type u_3) β†’ (I β†’ Ξ±) β†’+* I β†’ Ξ²
RingHom.compLeft
#align ring_hom.comp_left_apply 
RingHom.compLeft_apply: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : NonAssocSemiring Ξ±] [inst_1 : NonAssocSemiring Ξ²] (f : Ξ± β†’+* Ξ²) (I : Type u_3)
  (h : I β†’ Ξ±) (a : I), ↑(RingHom.compLeft f I) h a = (↑f ∘ h) a
RingHom.compLeft_apply

end RingHom