Pi instances for groups and monoids

This file defines instances for group, monoid, semigroup and related structures on Pi types.

ink

theorem Set.preimage_zero {α : Type u_1} {β : Type u_2} [inst : Zero β] (s : Set β) [inst : Decidable (0 ∈ s)] : 0 ⁻¹' s = if 0 ∈ s then Set.univ else ∅

ink

theorem Set.preimage_one {α : Type u_1} {β : Type u_2} [inst : One β] (s : Set β) [inst : Decidable (1 ∈ s)] : 1 ⁻¹' s = if 1 ∈ s then Set.univ else ∅

ink

instance Pi.addSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddSemigroup (f i)] : AddSemigroup ((i : I) → f i)

Equations

• Pi.addSemigroup = AddSemigroup.mk (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

def Pi.addSemigroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddSemigroup (f i)] : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)

Equations

• (_ : a + b + c = a + (b + c)) = (_ : a + b + c = a + (b + c))

ink

instance Pi.semigroup {I : Type u} {f : I → Type v} [inst : (i : I) → Semigroup (f i)] : Semigroup ((i : I) → f i)

Equations

• Pi.semigroup = Semigroup.mk (_ : ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c))

ink

instance Pi.addCommSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddCommSemigroup (f i)] : AddCommSemigroup ((i : I) → f i)

Equations

• Pi.addCommSemigroup = let src := Pi.addSemigroup; AddCommSemigroup.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.addCommSemigroup.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommSemigroup (f i)] : ∀ (a b : (i : I) → f i), a + b = b + a

Equations

• (_ : a + b = b + a) = (_ : a + b = b + a)

ink

def Pi.addCommSemigroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

instance Pi.commSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → CommSemigroup (f i)] : CommSemigroup ((i : I) → f i)

Equations

• Pi.commSemigroup = let src := Pi.semigroup; CommSemigroup.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

def Pi.addZeroClass.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddZeroClass (f i)] : ∀ (a : (i : I) → f i), 0 + a = a

Equations

• (_ : 0 + a = a) = (_ : 0 + a = a)

ink

def Pi.addZeroClass.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddZeroClass (f i)] : ∀ (a : (i : I) → f i), a + 0 = a

Equations

• (_ : a + 0 = a) = (_ : a + 0 = a)

ink

instance Pi.addZeroClass {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] : AddZeroClass ((i : I) → f i)

Equations

• Pi.addZeroClass = AddZeroClass.mk (_ : ∀ (a : (i : I) → f i), 0 + a = a) (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

instance Pi.mulOneClass {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] : MulOneClass ((i : I) → f i)

Equations

• Pi.mulOneClass = MulOneClass.mk (_ : ∀ (a : (i : I) → f i), 1 * a = a) (_ : ∀ (a : (i : I) → f i), a * 1 = a)

ink

def Pi.addMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddMonoid (f i)] : ∀ (x : (i : I) → f i), (fun n x i => n • x i) 0 x = 0

Equations

• (_ : (fun n x i => n • x i) 0 x = 0) = (_ : (fun n x i => n • x i) 0 x = 0)

ink

def Pi.addMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

def Pi.addMonoid.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddMonoid (f i)] : ∀ (n : ℕ) (x : (i : I) → f i), (fun n x i => n • x i) (n + 1) x = x + (fun n x i => n • x i) n x

Equations

• (_ : (fun n x i => n • x i) (n + 1) x = x + (fun n x i => n • x i) n x) = (_ : (fun n x i => n • x i) (n + 1) x = x + (fun n x i => n • x i) n x)

ink

def Pi.addMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

instance Pi.addMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddMonoid (f i)] : AddMonoid ((i : I) → f i)

Equations

• Pi.addMonoid = let src := Pi.addSemigroup; let src_1 := Pi.addZeroClass; AddMonoid.mk (_ : ∀ (a : (i : I) → f i), 0 + a = a) (_ : ∀ (a : (i : I) → f i), a + 0 = a) fun n x i => n • x i

ink

def Pi.addMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

instance Pi.monoid {I : Type u} {f : I → Type v} [inst : (i : I) → Monoid (f i)] : Monoid ((i : I) → f i)

Equations

• Pi.monoid = let src := Pi.semigroup; let src_1 := Pi.mulOneClass; Monoid.mk (_ : ∀ (a : (i : I) → f i), 1 * a = a) (_ : ∀ (a : (i : I) → f i), a * 1 = a) fun n x i => x i ^ n

ink

instance Pi.addMonoidWithOne {I : Type u} {f : I → Type v} [inst : (i : I) → AddMonoidWithOne (f i)] : AddMonoidWithOne ((i : I) → f i)

Equations

• Pi.addMonoidWithOne = let src := Pi.addMonoid; AddMonoidWithOne.mk

ink

def Pi.addCommMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

def Pi.addCommMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

def Pi.addCommMonoid.proof_5 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.addCommMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.addCommMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

instance Pi.addCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddCommMonoid (f i)] : AddCommMonoid ((i : I) → f i)

Equations

• Pi.addCommMonoid = let src := Pi.addMonoid; let src_1 := Pi.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

instance Pi.commMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → CommMonoid (f i)] : CommMonoid ((i : I) → f i)

Equations

• Pi.commMonoid = let src := Pi.monoid; let src_1 := Pi.commSemigroup; CommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

def Pi.subNegMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

def Pi.subNegMonoid.proof_6 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (a : (i : I) → f i), (fun z x i => z • x i) 0 a = 0

Equations

• (_ : (fun z x i => z • x i) 0 a = 0) = (_ : (fun z x i => z • x i) 0 a = 0)

ink

def Pi.subNegMonoid.proof_7 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (n : ℕ) (a : (i : I) → f i), (fun z x i => z • x i) (Int.ofNat (Nat.succ n)) a = a + (fun z x i => z • x i) (Int.ofNat n) a

Equations

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

ink

def Pi.subNegMonoid.proof_8 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (n : ℕ) (a : (i : I) → f i), (fun z x i => z • x i) (Int.negSucc n) a = -(fun z x i => z • x i) (↑(Nat.succ n)) a

Equations

• (_ : (fun z x i => z • x i) (Int.negSucc n) a = -(fun z x i => z • x i) (↑(Nat.succ n)) a) = (_ : (fun z x i => z • x i) (Int.negSucc n) a = -(fun z x i => z • x i) (↑(Nat.succ n)) a)

ink

def Pi.subNegMonoid.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (a b : (i : I) → f i), a - b = a + -b

Equations

• (_ : a - b = a + -b) = (_ : a - b = a + -b)

ink

def Pi.subNegMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

def Pi.subNegMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def Pi.subNegMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubNegMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

instance Pi.subNegMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → SubNegMonoid (f i)] : SubNegMonoid ((i : I) → f i)

Equations

• Pi.subNegMonoid = let src := Pi.addMonoid; SubNegMonoid.mk fun z x i => z • x i

ink

instance Pi.divInvMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → DivInvMonoid (f i)] : DivInvMonoid ((i : I) → f i)

Equations

• Pi.divInvMonoid = let src := Pi.monoid; DivInvMonoid.mk fun z x i => x i ^ z

ink

instance Pi.involutiveNeg {I : Type u} {f : I → Type v} [inst : (i : I) → InvolutiveNeg (f i)] : InvolutiveNeg ((i : I) → f i)

Equations

• Pi.involutiveNeg = InvolutiveNeg.mk (_ : ∀ (x : (i : I) → f i), - -x = x)

ink

def Pi.involutiveNeg.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → InvolutiveNeg (f i)] : ∀ (x : (i : I) → f i), - -x = x

Equations

• (_ : - -x = x) = (_ : - -x = x)

ink

instance Pi.involutiveInv {I : Type u} {f : I → Type v} [inst : (i : I) → InvolutiveInv (f i)] : InvolutiveInv ((i : I) → f i)

Equations

• Pi.involutiveInv = InvolutiveInv.mk (_ : ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x)

ink

def Pi.subtractionMonoid.proof_5 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → SubtractionMonoid (f i)] (x : (i : I) → f i) : - -x = x

Equations

• (_ : ∀ (x : (i : I) → f i), - -x = x) = (_ : ∀ (x : (i : I) → f i), - -x = x)

ink

def Pi.subtractionMonoid.proof_6 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] : ∀ (a b : (i : I) → f i), -(a + b) = -b + -a

Equations

• (_ : -(a + b) = -b + -a) = (_ : -(a + b) = -b + -a)

ink

def Pi.subtractionMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a - b = a + -b

Equations

• (_ : ∀ (a b : (i : I) → f i), a - b = a + -b) = (_ : ∀ (a b : (i : I) → f i), a - b = a + -b)

ink

def Pi.subtractionMonoid.proof_7 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] : ∀ (a b : (i : I) → f i), a + b = 0 → -a = b

Equations

• (_ : -a = b) = (_ : -a = b)

ink

instance Pi.subtractionMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → SubtractionMonoid (f i)] : SubtractionMonoid ((i : I) → f i)

Equations

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

ink

def Pi.subtractionMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

Equations

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

ink

def Pi.subtractionMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) : SubNegMonoid.zsmul 0 a = 0

Equations

• (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0)

ink

def Pi.subtractionMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionMonoid (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

Equations

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

ink

instance Pi.divisionMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → DivisionMonoid (f i)] : DivisionMonoid ((i : I) → f i)

Equations

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

ink

def Pi.subtractionCommMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : -(a + b) = -b + -a

Equations

• (_ : ∀ (a b : (i : I) → f i), -(a + b) = -b + -a) = (_ : ∀ (a b : (i : I) → f i), -(a + b) = -b + -a)

ink

def Pi.subtractionCommMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionCommMonoid (f i)] (x : (i : I) → f i) : - -x = x

Equations

• (_ : ∀ (x : (i : I) → f i), - -x = x) = (_ : ∀ (x : (i : I) → f i), - -x = x)

ink

instance Pi.subtractionCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → SubtractionCommMonoid (f i)] : SubtractionCommMonoid ((i : I) → f i)

Equations

• Pi.subtractionCommMonoid = let src := Pi.subtractionMonoid; let src_1 := Pi.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.subtractionCommMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → SubtractionCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = 0 → -a = b

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = 0 → -a = b) = (_ : ∀ (a b : (i : I) → f i), a + b = 0 → -a = b)

ink

def Pi.subtractionCommMonoid.proof_4 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → SubtractionCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

instance Pi.instDivisionCommMonoidForAll {I : Type u} {f : I → Type v} [inst : (i : I) → DivisionCommMonoid (f i)] : DivisionCommMonoid ((i : I) → f i)

Equations

• Pi.instDivisionCommMonoidForAll = let src := Pi.divisionMonoid; let src_1 := Pi.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

def Pi.addGroup.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddGroup (f i)] (a : (i : I) → f i) : SubNegMonoid.zsmul 0 a = 0

Equations

• (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0)

ink

def Pi.addGroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a - b = a + -b

Equations

• (_ : ∀ (a b : (i : I) → f i), a - b = a + -b) = (_ : ∀ (a b : (i : I) → f i), a - b = a + -b)

ink

def Pi.addGroup.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddGroup (f i)] : ∀ (a : (i : I) → f i), -a + a = 0

Equations

• (_ : -a + a = 0) = (_ : -a + a = 0)

ink

instance Pi.addGroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddGroup (f i)] : AddGroup ((i : I) → f i)

Equations

• Pi.addGroup = let src := Pi.subNegMonoid; AddGroup.mk (_ : ∀ (a : (i : I) → f i), -a + a = 0)

ink

def Pi.addGroup.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddGroup (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

Equations

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

ink

def Pi.addGroup.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddGroup (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

Equations

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

ink

instance Pi.group {I : Type u} {f : I → Type v} [inst : (i : I) → Group (f i)] : Group ((i : I) → f i)

Equations

• Pi.group = let src := Pi.divInvMonoid; Group.mk (_ : ∀ (a : (i : I) → f i), a⁻¹ * a = 1)

ink

instance Pi.addGroupWithOne {I : Type u} {f : I → Type v} [inst : (i : I) → AddGroupWithOne (f i)] : AddGroupWithOne ((i : I) → f i)

Equations

• Pi.addGroupWithOne = let src := Pi.addGroup; let src_1 := Pi.addMonoidWithOne; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : (i : I) → f i), -a + a = 0)

ink

instance Pi.addCommGroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddCommGroup (f i)] : AddCommGroup ((i : I) → f i)

Equations

• Pi.addCommGroup = let src := Pi.addGroup; let src_1 := Pi.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.addCommGroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCommGroup (f i)] (a : (i : I) → f i) : -a + a = 0

Equations

• (_ : ∀ (a : (i : I) → f i), -a + a = 0) = (_ : ∀ (a : (i : I) → f i), -a + a = 0)

ink

def Pi.addCommGroup.proof_2 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → AddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

instance Pi.commGroup {I : Type u} {f : I → Type v} [inst : (i : I) → CommGroup (f i)] : CommGroup ((i : I) → f i)

Equations

• Pi.commGroup = let src := Pi.group; let src_1 := Pi.commMonoid; CommGroup.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

def Pi.addLeftCancelSemigroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

def Pi.addLeftCancelSemigroup.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelSemigroup (f i)] : ∀ (a b c : (i : I) → f i), a + b = a + c → b = c

Equations

• (_ : b = c) = (_ : b = c)

ink

instance Pi.addLeftCancelSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddLeftCancelSemigroup (f i)] : AddLeftCancelSemigroup ((i : I) → f i)

Equations

• Pi.addLeftCancelSemigroup = let src := Pi.addSemigroup; AddLeftCancelSemigroup.mk (_ : ∀ (a b c : (i : I) → f i), a + b = a + c → b = c)

ink

instance Pi.leftCancelSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → LeftCancelSemigroup (f i)] : LeftCancelSemigroup ((i : I) → f i)

Equations

• Pi.leftCancelSemigroup = let src := Pi.semigroup; LeftCancelSemigroup.mk (_ : ∀ (a b c : (i : I) → f i), a * b = a * c → b = c)

ink

def Pi.addRightCancelSemigroup.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

instance Pi.addRightCancelSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → AddRightCancelSemigroup (f i)] : AddRightCancelSemigroup ((i : I) → f i)

Equations

• Pi.addRightCancelSemigroup = let src := Pi.addSemigroup; AddRightCancelSemigroup.mk (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c)

ink

def Pi.addRightCancelSemigroup.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelSemigroup (f i)] : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c

Equations

• (_ : a = c) = (_ : a = c)

ink

instance Pi.rightCancelSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → RightCancelSemigroup (f i)] : RightCancelSemigroup ((i : I) → f i)

Equations

• Pi.rightCancelSemigroup = let src := Pi.semigroup; RightCancelSemigroup.mk (_ : ∀ (a b c : (i : I) → f i), a * b = c * b → a = c)

ink

def Pi.addLeftCancelMonoid.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def Pi.addLeftCancelMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b = a + c → b = c

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b = a + c → b = c) = (_ : ∀ (a b c : (i : I) → f i), a + b = a + c → b = c)

ink

def Pi.addLeftCancelMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

instance Pi.addLeftCancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddLeftCancelMonoid (f i)] : AddLeftCancelMonoid ((i : I) → f i)

Equations

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

ink

def Pi.addLeftCancelMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.addLeftCancelMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

instance Pi.leftCancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → LeftCancelMonoid (f i)] : LeftCancelMonoid ((i : I) → f i)

Equations

• Pi.leftCancelMonoid = let src := Pi.leftCancelSemigroup; let src_1 := Pi.monoid; LeftCancelMonoid.mk (_ : ∀ (a : (i : I) → f i), 1 * a = a) (_ : ∀ (a : (i : I) → f i), a * 1 = a) Monoid.npow

ink

def Pi.addRightCancelMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

def Pi.addRightCancelMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b = c + b → a = c

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c) = (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c)

ink

def Pi.addRightCancelMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

def Pi.addRightCancelMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.addRightCancelMonoid.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddRightCancelMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

instance Pi.addRightCancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddRightCancelMonoid (f i)] : AddRightCancelMonoid ((i : I) → f i)

Equations

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

ink

instance Pi.rightCancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → RightCancelMonoid (f i)] : RightCancelMonoid ((i : I) → f i)

Equations

• Pi.rightCancelMonoid = let src := Pi.rightCancelSemigroup; let src_1 := Pi.monoid; RightCancelMonoid.mk (_ : ∀ (a : (i : I) → f i), 1 * a = a) (_ : ∀ (a : (i : I) → f i), a * 1 = a) Monoid.npow

ink

def Pi.addCancelMonoid.proof_5 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b = c + b → a = c

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c) = (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c)

ink

instance Pi.addCancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddCancelMonoid (f i)] : AddCancelMonoid ((i : I) → f i)

Equations

• Pi.addCancelMonoid = let src := Pi.addLeftCancelMonoid; let src_1 := Pi.addRightCancelMonoid; AddCancelMonoid.mk (_ : ∀ (a b c : (i : I) → f i), a + b = c + b → a = c)

ink

def Pi.addCancelMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelMonoid (f i)] (x : (i : I) → f i) : AddLeftCancelMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0)

ink

def Pi.addCancelMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddLeftCancelMonoid.nsmul (n + 1) x = x + AddLeftCancelMonoid.nsmul n x

Equations

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

ink

def Pi.addCancelMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.addCancelMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

instance Pi.cancelMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → CancelMonoid (f i)] : CancelMonoid ((i : I) → f i)

Equations

• Pi.cancelMonoid = let src := Pi.leftCancelMonoid; let src_1 := Pi.rightCancelMonoid; CancelMonoid.mk (_ : ∀ (a b c : (i : I) → f i), a * b = c * b → a = c)

ink

def Pi.addCancelCommMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelCommMonoid (f i)] (x : (i : I) → f i) : AddLeftCancelMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0)

ink

def Pi.addCancelCommMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.addCancelCommMonoid.proof_5 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

instance Pi.addCancelCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddCancelCommMonoid (f i)] : AddCancelCommMonoid ((i : I) → f i)

Equations

• Pi.addCancelCommMonoid = let src := Pi.addLeftCancelMonoid; let src_1 := Pi.addCommMonoid; AddCancelCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.addCancelCommMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelCommMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddLeftCancelMonoid.nsmul (n + 1) x = x + AddLeftCancelMonoid.nsmul n x

Equations

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

ink

def Pi.addCancelCommMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

instance Pi.cancelCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → CancelCommMonoid (f i)] : CancelCommMonoid ((i : I) → f i)

Equations

• Pi.cancelCommMonoid = let src := Pi.leftCancelMonoid; let src_1 := Pi.commMonoid; CancelCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

instance Pi.mulZeroClass {I : Type u} {f : I → Type v} [inst : (i : I) → MulZeroClass (f i)] : MulZeroClass ((i : I) → f i)

Equations

• Pi.mulZeroClass = MulZeroClass.mk (_ : ∀ (a : (i : I) → f i), 0 * a = 0) (_ : ∀ (a : (i : I) → f i), a * 0 = 0)

ink

instance Pi.mulZeroOneClass {I : Type u} {f : I → Type v} [inst : (i : I) → MulZeroOneClass (f i)] : MulZeroOneClass ((i : I) → f i)

Equations

• Pi.mulZeroOneClass = let src := Pi.mulZeroClass; let src_1 := Pi.mulOneClass; MulZeroOneClass.mk (_ : ∀ (a : (i : I) → f i), 0 * a = 0) (_ : ∀ (a : (i : I) → f i), a * 0 = 0)

ink

instance Pi.monoidWithZero {I : Type u} {f : I → Type v} [inst : (i : I) → MonoidWithZero (f i)] : MonoidWithZero ((i : I) → f i)

Equations

• Pi.monoidWithZero = let src := Pi.monoid; let src_1 := Pi.mulZeroClass; MonoidWithZero.mk (_ : ∀ (a : (i : I) → f i), 0 * a = 0) (_ : ∀ (a : (i : I) → f i), a * 0 = 0)

ink

instance Pi.commMonoidWithZero {I : Type u} {f : I → Type v} [inst : (i : I) → CommMonoidWithZero (f i)] : CommMonoidWithZero ((i : I) → f i)

Equations

• Pi.commMonoidWithZero = let src := Pi.monoidWithZero; let src_1 := Pi.commMonoid; CommMonoidWithZero.mk (_ : ∀ (a : (i : I) → f i), 0 * a = 0) (_ : ∀ (a : (i : I) → f i), a * 0 = 0)

ink

instance Pi.semigroupWithZero {I : Type u} {f : I → Type v} [inst : (i : I) → SemigroupWithZero (f i)] : SemigroupWithZero ((i : I) → f i)

Equations

• Pi.semigroupWithZero = let src := Pi.semigroup; let src_1 := Pi.mulZeroClass; SemigroupWithZero.mk (_ : ∀ (a : (i : I) → f i), 0 * a = 0) (_ : ∀ (a : (i : I) → f i), a * 0 = 0)

ink

theorem AddHom.coe_add {M : Type u_1} {N : Type u_2} : ∀ {x : Add M} {x_1 : AddCommSemigroup N} (f g : AddHom M N), ↑f + ↑g = fun x_2 => ↑f x_2 + ↑g x_2

ink

theorem MulHom.coe_mul {M : Type u_1} {N : Type u_2} : ∀ {x : Mul M} {x_1 : CommSemigroup N} (f g : M →ₙ* N), ↑f * ↑g = fun x_2 => ↑f x_2 * ↑g x_2

ink

def Pi.addHom {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → Add (f i)] [inst : Add γ] (g : (i : I) → AddHom γ (f i)) : AddHom γ ((i : I) → f i)

A family of AddHom's f a : γ → β a→ β a defines an AddHom Pi.addHom f : γ → Π a, β a→ Π a, β a given by Pi.addHom f x b = f b x.

Equations

• Pi.addHom g = { toFun := fun x i => ↑(g i) x, map_add' := (_ : ∀ (x y : γ), (fun x i => ↑(g i) x) (x + y) = (fun x i => ↑(g i) x) x + (fun x i => ↑(g i) x) y) }

ink

def Pi.addHom.proof_1 {I : Type u_1} {f : I → Type u_2} {γ : Type u_3} [inst : (i : I) → Add (f i)] [inst : Add γ] (g : (i : I) → AddHom γ (f i)) (x : γ) (y : γ) : (fun x i => ↑(g i) x) (x + y) = (fun x i => ↑(g i) x) x + (fun x i => ↑(g i) x) y

Equations

• (_ : (fun x i => ↑(g i) x) (x + y) = (fun x i => ↑(g i) x) x + (fun x i => ↑(g i) x) y) = (_ : (fun x i => ↑(g i) x) (x + y) = (fun x i => ↑(g i) x) x + (fun x i => ↑(g i) x) y)

ink

@[simp]

theorem Pi.mulHom_apply {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → Mul (f i)] [inst : Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) : ↑(Pi.mulHom g) x i = ↑(g i) x

ink

@[simp]

theorem Pi.addHom_apply {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → Add (f i)] [inst : Add γ] (g : (i : I) → AddHom γ (f i)) (x : γ) (i : I) : ↑(Pi.addHom g) x i = ↑(g i) x

ink

def Pi.mulHom {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → Mul (f i)] [inst : Mul γ] (g : (i : I) → γ →ₙ* f i) : γ →ₙ* (i : I) → f i

A family of MulHom's f a : γ →ₙ* β a→ₙ* β a defines a MulHom Pi.mulHom f : γ →ₙ* Π a, β a→ₙ* Π a, β a given by Pi.mulHom f x b = f b x.

Equations

• Pi.mulHom g = { toFun := fun x i => ↑(g i) x, map_mul' := (_ : ∀ (x y : γ), (fun x i => ↑(g i) x) (x * y) = (fun x i => ↑(g i) x) x * (fun x i => ↑(g i) x) y) }

ink

abbrev Pi.addHom_injective.match_1 {I : Type u_1} (motive : Nonempty I → Prop) : (x : Nonempty I) → ((i : I) → motive (_ : Nonempty I)) → motive x

Equations

• Pi.addHom_injective.match_1 motive x h_1 = Nonempty.casesOn x fun val => h_1 val

ink

theorem Pi.addHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [inst : Nonempty I] [inst : (i : I) → Add (f i)] [inst : Add γ] (g : (i : I) → AddHom γ (f i)) (hg : ∀ (i : I), Function.Injective ↑(g i)) : Function.Injective ↑(Pi.addHom g)

ink

theorem Pi.mulHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [inst : Nonempty I] [inst : (i : I) → Mul (f i)] [inst : Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) : Function.Injective ↑(Pi.mulHom g)

ink

def Pi.addMonoidHom.proof_2 {I : Type u_1} {f : I → Type u_2} {γ : Type u_3} [inst : (i : I) → AddZeroClass (f i)] [inst : AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (y : γ) : AddHom.toFun (Pi.addHom fun i => ↑(g i)) (x + y) = AddHom.toFun (Pi.addHom fun i => ↑(g i)) x + AddHom.toFun (Pi.addHom fun i => ↑(g i)) y

Equations

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

ink

def Pi.addMonoidHom.proof_1 {I : Type u_1} {f : I → Type u_2} {γ : Type u_3} [inst : (i : I) → AddZeroClass (f i)] [inst : AddZeroClass γ] (g : (i : I) → γ →+ f i) : (fun x i => ↑(g i) x) 0 = 0

Equations

• (_ : (fun x i => ↑(g i) x) 0 = 0) = (_ : (fun x i => ↑(g i) x) 0 = 0)

ink

def Pi.addMonoidHom {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → AddZeroClass (f i)] [inst : AddZeroClass γ] (g : (i : I) → γ →+ f i) : γ →+ (i : I) → f i

A family of additive monoid homomorphisms f a : γ →+ β a→+ β a defines a monoid homomorphism Pi.addMonoidHom f : γ →+ Π a, β a→+ Π a, β a given by Pi.addMonoidHom f x b = f b x.

Equations

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

ink

@[simp]

theorem Pi.monoidHom_apply {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → MulOneClass (f i)] [inst : MulOneClass γ] (g : (i : I) → γ →* f i) (x : γ) (i : I) : ↑(Pi.monoidHom g) x i = ↑(g i) x

ink

@[simp]

theorem Pi.addMonoidHom_apply {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → AddZeroClass (f i)] [inst : AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (i : I) : ↑(Pi.addMonoidHom g) x i = ↑(g i) x

ink

def Pi.monoidHom {I : Type u} {f : I → Type v} {γ : Type w} [inst : (i : I) → MulOneClass (f i)] [inst : MulOneClass γ] (g : (i : I) → γ →* f i) : γ →* (i : I) → f i

A family of monoid homomorphisms f a : γ →* β a→* β a defines a monoid homomorphism Pi.monoidHom f : γ →* Π a, β a→* Π a, β a given by Pi.monoidHom f x b = f b x.

Equations

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

ink

theorem Pi.addMonoidHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [inst : Nonempty I] [inst : (i : I) → AddZeroClass (f i)] [inst : AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) : Function.Injective ↑(Pi.addMonoidHom g)

ink

theorem Pi.monoidHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [inst : Nonempty I] [inst : (i : I) → MulOneClass (f i)] [inst : MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) : Function.Injective ↑(Pi.monoidHom g)

ink

def Pi.evalAddHom.proof_1 {I : Type u_2} (f : I → Type u_1) [inst : (i : I) → Add (f i)] (i : I) : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x_1 i = x i + x_1 i

Equations

• (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i) = (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i)

ink

def Pi.evalAddHom {I : Type u} (f : I → Type v) [inst : (i : I) → Add (f i)] (i : I) : AddHom ((i : I) → f i) (f i)

Evaluation of functions into an indexed collection of additive semigroups at a point is an additive semigroup homomorphism. This is Function.eval i as an AddHom.

Equations

• Pi.evalAddHom f i = { toFun := fun g => g i, map_add' := (_ : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x_1 i = x i + x_1 i) }

ink

@[simp]

theorem Pi.evalAddHom_apply {I : Type u} (f : I → Type v) [inst : (i : I) → Add (f i)] (i : I) (g : (i : I) → f i) : ↑(Pi.evalAddHom f i) g = g i

ink

@[simp]

theorem Pi.evalMulHom_apply {I : Type u} (f : I → Type v) [inst : (i : I) → Mul (f i)] (i : I) (g : (i : I) → f i) : ↑(Pi.evalMulHom f i) g = g i

ink

def Pi.evalMulHom {I : Type u} (f : I → Type v) [inst : (i : I) → Mul (f i)] (i : I) : ((i : I) → f i) →ₙ* f i

Evaluation of functions into an indexed collection of semigroups at a point is a semigroup homomorphism. This is Function.eval i as a MulHom.

Equations

• Pi.evalMulHom f i = { toFun := fun g => g i, map_mul' := (_ : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) * ((i : I) → f i)) ((i : I) → f i) instHMul x x_1 i = x i * x_1 i) }

ink

def Pi.constAddHom.proof_1 (α : Type u_1) (β : Type u_2) [inst : Add β] : ∀ (x x_1 : β), Function.const α (x + x_1) = Function.const α (x + x_1)

Equations

• (_ : Function.const α (x + x) = Function.const α (x + x)) = (_ : Function.const α (x + x) = Function.const α (x + x))

ink

def Pi.constAddHom (α : Type u_1) (β : Type u_2) [inst : Add β] : AddHom β (α → β)

Function.const as an AddHom.

Equations

• Pi.constAddHom α β = { toFun := Function.const α, map_add' := (_ : ∀ (x x_1 : β), Function.const α (x + x_1) = Function.const α (x + x_1)) }

ink

@[simp]

theorem Pi.constAddHom_apply (α : Type u_1) (β : Type u_2) [inst : Add β] (a : β) : ∀ (a : α), ↑(Pi.constAddHom α β) a a = Function.const α a a

ink

@[simp]

theorem Pi.constMulHom_apply (α : Type u_1) (β : Type u_2) [inst : Mul β] (a : β) : ∀ (a : α), ↑(Pi.constMulHom α β) a a = Function.const α a a

ink

def Pi.constMulHom (α : Type u_1) (β : Type u_2) [inst : Mul β] : β →ₙ* α → β

Function.const as a MulHom.

Equations

• Pi.constMulHom α β = { toFun := Function.const α, map_mul' := (_ : ∀ (x x_1 : β), Function.const α (x * x_1) = Function.const α (x * x_1)) }

ink

def AddHom.coeFn.proof_1 (α : Type u_1) (β : Type u_2) [inst : Add α] [inst : AddCommSemigroup β] : ∀ (x x_1 : AddHom α β), (fun g => ↑g) (x + x_1) = (fun g => ↑g) (x + x_1)

Equations

• (_ : (fun g => ↑g) (x + x) = (fun g => ↑g) (x + x)) = (_ : (fun g => ↑g) (x + x) = (fun g => ↑g) (x + x))

ink

def AddHom.coeFn (α : Type u_1) (β : Type u_2) [inst : Add α] [inst : AddCommSemigroup β] : AddHom (AddHom α β) (α → β)

Coercion of an AddHom into a function is itself an AddHom.

See also AddHom.eval.

Equations

• AddHom.coeFn α β = { toFun := fun g => ↑g, map_add' := (_ : ∀ (x x_1 : AddHom α β), (fun g => ↑g) (x + x_1) = (fun g => ↑g) (x + x_1)) }

ink

@[simp]

theorem AddHom.coeFn_apply (α : Type u_1) (β : Type u_2) [inst : Add α] [inst : AddCommSemigroup β] (g : AddHom α β) (a : α) : ↑(AddHom.coeFn α β) g a = ↑g a

ink

@[simp]

theorem MulHom.coeFn_apply (α : Type u_1) (β : Type u_2) [inst : Mul α] [inst : CommSemigroup β] (g : α →ₙ* β) (a : α) : ↑(MulHom.coeFn α β) g a = ↑g a

ink

def MulHom.coeFn (α : Type u_1) (β : Type u_2) [inst : Mul α] [inst : CommSemigroup β] : (α →ₙ* β) →ₙ* α → β

Coercion of a MulHom into a function is itself a MulHom.

See also MulHom.eval.

Equations

• MulHom.coeFn α β = { toFun := fun g => ↑g, map_mul' := (_ : ∀ (x x_1 : α →ₙ* β), (fun g => ↑g) (x * x_1) = (fun g => ↑g) (x * x_1)) }

ink

def AddHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [inst : Add α] [inst : Add β] (f : AddHom α β) (I : Type u_1) : ∀ (x x_1 : I → α), (fun h => ↑f ∘ h) (x + x_1) = (fun h => ↑f ∘ h) x + (fun h => ↑f ∘ h) x_1

Equations

• (_ : (fun h => ↑f ∘ h) (x + x) = (fun h => ↑f ∘ h) x + (fun h => ↑f ∘ h) x) = (_ : (fun h => ↑f ∘ h) (x + x) = (fun h => ↑f ∘ h) x + (fun h => ↑f ∘ h) x)

ink

def AddHom.compLeft {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (f : AddHom α β) (I : Type u_3) : AddHom (I → α) (I → β)

Additive semigroup homomorphism between the function spaces I → α→ α and I → β→ β, induced by an additive semigroup homomorphism f between α and β

Equations

• AddHom.compLeft f I = { toFun := fun h => ↑f ∘ h, map_add' := (_ : ∀ (x x_1 : I → α), (fun h => ↑f ∘ h) (x + x_1) = (fun h => ↑f ∘ h) x + (fun h => ↑f ∘ h) x_1) }

ink

@[simp]

theorem MulHom.compLeft_apply {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Mul β] (f : α →ₙ* β) (I : Type u_3) (h : I → α) : ∀ (a : I), ↑(MulHom.compLeft f I) h a = (↑f ∘ h) a

ink

@[simp]

theorem AddHom.compLeft_apply {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (f : AddHom α β) (I : Type u_3) (h : I → α) : ∀ (a : I), ↑(AddHom.compLeft f I) h a = (↑f ∘ h) a

ink

def MulHom.compLeft {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Mul β] (f : α →ₙ* β) (I : Type u_3) : (I → α) →ₙ* I → β

Semigroup homomorphism between the function spaces I → α→ α and I → β→ β, induced by a semigroup homomorphism f between α and β.

Equations

• MulHom.compLeft f I = { toFun := fun h => ↑f ∘ h, map_mul' := (_ : ∀ (x x_1 : I → α), (fun h => ↑f ∘ h) (x * x_1) = (fun h => ↑f ∘ h) x * (fun h => ↑f ∘ h) x_1) }

ink

def Pi.evalAddMonoidHom.proof_2 {I : Type u_2} (f : I → Type u_1) [inst : (i : I) → AddZeroClass (f i)] (i : I) : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x_1 i = x i + x_1 i

Equations

• (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i) = (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i)

ink

def Pi.evalAddMonoidHom {I : Type u} (f : I → Type v) [inst : (i : I) → AddZeroClass (f i)] (i : I) : ((i : I) → f i) →+ f i

Evaluation of functions into an indexed collection of additive monoids at a point is an additive monoid homomorphism. This is Function.eval i as an AddMonoidHom.

Equations

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

ink

def Pi.evalAddMonoidHom.proof_1 {I : Type u_2} (f : I → Type u_1) [inst : (i : I) → AddZeroClass (f i)] (i : I) : OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0

Equations

• (_ : OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0) = (_ : OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0)

ink

@[simp]

theorem Pi.evalMonoidHom_apply {I : Type u} (f : I → Type v) [inst : (i : I) → MulOneClass (f i)] (i : I) (g : (i : I) → f i) : ↑(Pi.evalMonoidHom f i) g = g i

ink

@[simp]

theorem Pi.evalAddMonoidHom_apply {I : Type u} (f : I → Type v) [inst : (i : I) → AddZeroClass (f i)] (i : I) (g : (i : I) → f i) : ↑(Pi.evalAddMonoidHom f i) g = g i

ink

def Pi.evalMonoidHom {I : Type u} (f : I → Type v) [inst : (i : I) → MulOneClass (f i)] (i : I) : ((i : I) → f i) →* f i

Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism. This is Function.eval i as a MonoidHom.

Equations

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

ink

def Pi.constAddMonoidHom.proof_2 (α : Type u_1) (β : Type u_2) [inst : AddZeroClass β] : ∀ (x x_1 : β), ZeroHom.toFun { toFun := Function.const α, map_zero' := (_ : Function.const α 0 = Function.const α 0) } (x + x_1) = ZeroHom.toFun { toFun := Function.const α, map_zero' := (_ : Function.const α 0 = Function.const α 0) } (x + x_1)

Equations

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

ink

def Pi.constAddMonoidHom.proof_1 (α : Type u_1) (β : Type u_2) [inst : AddZeroClass β] : Function.const α 0 = Function.const α 0

Equations

• (_ : Function.const α 0 = Function.const α 0) = (_ : Function.const α 0 = Function.const α 0)

ink

def Pi.constAddMonoidHom (α : Type u_1) (β : Type u_2) [inst : AddZeroClass β] : β →+ α → β

Function.const as an AddMonoidHom.

Equations

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

ink

@[simp]

theorem Pi.constAddMonoidHom_apply (α : Type u_1) (β : Type u_2) [inst : AddZeroClass β] (a : β) : ∀ (a : α), ↑(Pi.constAddMonoidHom α β) a a = Function.const α a a

ink

@[simp]

theorem Pi.constMonoidHom_apply (α : Type u_1) (β : Type u_2) [inst : MulOneClass β] (a : β) : ∀ (a : α), ↑(Pi.constMonoidHom α β) a a = Function.const α a a

ink

def Pi.constMonoidHom (α : Type u_1) (β : Type u_2) [inst : MulOneClass β] : β →* α → β

Function.const as a MonoidHom.

Equations

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

ink

def AddMonoidHom.coeFn (α : Type u_1) (β : Type u_2) [inst : AddZeroClass α] [inst : AddCommMonoid β] : (α →+ β) →+ α → β

Coercion of an AddMonoidHom into a function is itself a AddMonoidHom.

See also AddMonoidHom.eval.

Equations

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

ink

def AddMonoidHom.coeFn.proof_1 (α : Type u_1) (β : Type u_2) [inst : AddZeroClass α] [inst : AddCommMonoid β] : (fun g => ↑g) 0 = (fun g => ↑g) 0

Equations

• (_ : (fun g => ↑g) 0 = (fun g => ↑g) 0) = (_ : (fun g => ↑g) 0 = (fun g => ↑g) 0)

ink

def AddMonoidHom.coeFn.proof_2 (α : Type u_1) (β : Type u_2) [inst : AddZeroClass α] [inst : AddCommMonoid β] : ∀ (x x_1 : α →+ β), ZeroHom.toFun { toFun := fun g => ↑g, map_zero' := (_ : (fun g => ↑g) 0 = (fun g => ↑g) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun g => ↑g, map_zero' := (_ : (fun g => ↑g) 0 = (fun g => ↑g) 0) } (x + x_1)

Equations

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

ink

@[simp]

theorem MonoidHom.coeFn_apply (α : Type u_1) (β : Type u_2) [inst : MulOneClass α] [inst : CommMonoid β] (g : α →* β) (a : α) : ↑(MonoidHom.coeFn α β) g a = ↑g a

ink

@[simp]

theorem AddMonoidHom.coeFn_apply (α : Type u_1) (β : Type u_2) [inst : AddZeroClass α] [inst : AddCommMonoid β] (g : α →+ β) (a : α) : ↑(AddMonoidHom.coeFn α β) g a = ↑g a

ink

def MonoidHom.coeFn (α : Type u_1) (β : Type u_2) [inst : MulOneClass α] [inst : CommMonoid β] : (α →* β) →* α → β

Coercion of a MonoidHom into a function is itself a MonoidHom.

See also MonoidHom.eval.

Equations

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

ink

def AddMonoidHom.compLeft.proof_2 {α : Type u_3} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (I : Type u_1) : ∀ (x x_1 : I → α), ZeroHom.toFun { toFun := fun h => ↑f ∘ h, map_zero' := (_ : (fun h => ↑f ∘ h) 0 = 0) } (x + x_1) = ZeroHom.toFun { toFun := fun h => ↑f ∘ h, map_zero' := (_ : (fun h => ↑f ∘ h) 0 = 0) } x + ZeroHom.toFun { toFun := fun h => ↑f ∘ h, map_zero' := (_ : (fun h => ↑f ∘ h) 0 = 0) } x_1

Equations

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

ink

def AddMonoidHom.compLeft {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (I : Type u_3) : (I → α) →+ I → β

Additive monoid homomorphism between the function spaces I → α→ α and I → β→ β, induced by an additive monoid homomorphism f between α and β

Equations

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

ink

def AddMonoidHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (I : Type u_1) : (fun h => ↑f ∘ h) 0 = 0

Equations

• (_ : (fun h => ↑f ∘ h) 0 = 0) = (_ : (fun h => ↑f ∘ h) 0 = 0)

ink

@[simp]

theorem AddMonoidHom.compLeft_apply {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (I : Type u_3) (h : I → α) : ∀ (a : I), ↑(AddMonoidHom.compLeft f I) h a = (↑f ∘ h) a

ink

@[simp]

theorem MonoidHom.compLeft_apply {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst : MulOneClass β] (f : α →* β) (I : Type u_3) (h : I → α) : ∀ (a : I), ↑(MonoidHom.compLeft f I) h a = (↑f ∘ h) a

ink

def MonoidHom.compLeft {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst : MulOneClass β] (f : α →* β) (I : Type u_3) : (I → α) →* I → β

Monoid homomorphism between the function spaces I → α→ α and I → β→ β, induced by a monoid homomorphism f between α and β.

Equations

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

ink

def ZeroHom.single.proof_1 {I : Type u_1} (f : I → Type u_2) [inst : DecidableEq I] [inst : (i : I) → Zero (f i)] (i : I) : Pi.single i 0 = 0

Equations

• (_ : Pi.single i 0 = 0) = (_ : Pi.single i 0 = 0)

ink

def ZeroHom.single {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → Zero (f i)] (i : I) : ZeroHom (f i) ((i : I) → f i)

The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the ZeroHom version of Pi.single.

Equations

• ZeroHom.single f i = { toFun := Pi.single i, map_zero' := (_ : Pi.single i 0 = 0) }

ink

def OneHom.single {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → One (f i)] (i : I) : OneHom (f i) ((i : I) → f i)

The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the OneHom version of Pi.mulSingle.

Equations

• OneHom.single f i = { toFun := Pi.mulSingle i, map_one' := (_ : Pi.mulSingle i 1 = 1) }

ink

@[simp]

theorem ZeroHom.single_apply {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → Zero (f i)] (i : I) (x : f i) : ↑(ZeroHom.single f i) x = Pi.single i x

ink

@[simp]

theorem OneHom.single_apply {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → One (f i)] (i : I) (x : f i) : ↑(OneHom.single f i) x = Pi.mulSingle i x

ink

def AddMonoidHom.single {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (i : I) : f i →+ (i : I) → f i

The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.

This is the AddMonoidHom version of Pi.single.

Equations

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

ink

def AddMonoidHom.single.proof_2 {I : Type u_1} (f : I → Type u_2) [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (i : I) (x₁ : f i) (x₂ : f i) : Pi.single i (x₁ + x₂) = fun j => Pi.single i x₁ j + Pi.single i x₂ j

Equations

• (_ : ∀ (x₁ x₂ : f i), Pi.single i (x₁ + x₂) = fun j => Pi.single i x₁ j + Pi.single i x₂ j) = (_ : ∀ (x₁ x₂ : f i), Pi.single i (x₁ + x₂) = fun j => Pi.single i x₁ j + Pi.single i x₂ j)

ink

def AddMonoidHom.single.proof_1 {I : Type u_1} (f : I → Type u_2) [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (i : I) : ZeroHom.toFun (ZeroHom.single f i) 0 = 0

Equations

• (_ : ZeroHom.toFun (ZeroHom.single f i) 0 = 0) = (_ : ZeroHom.toFun (ZeroHom.single f i) 0 = 0)

ink

def MonoidHom.single {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → MulOneClass (f i)] (i : I) : f i →* (i : I) → f i

The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point.

This is the MonoidHom version of Pi.mulSingle.

Equations

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

ink

@[simp]

theorem AddMonoidHom.single_apply {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (i : I) (x : f i) : ↑(AddMonoidHom.single f i) x = Pi.single i x

ink

@[simp]

theorem MonoidHom.single_apply {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → MulOneClass (f i)] (i : I) (x : f i) : ↑(MonoidHom.single f i) x = Pi.mulSingle i x

ink

@[simp]

theorem MulHom.single_apply {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → MulZeroClass (f i)] (i : I) (x : f i) (j : I) : ↑(MulHom.single f i) x j = Pi.single i x j

ink

def MulHom.single {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst : (i : I) → MulZeroClass (f i)] (i : I) : f i →ₙ* (i : I) → f i

The multiplicative homomorphism including a single MulZeroClass into a dependent family of MulZeroClasses, as functions supported at a point.

This is the MulHom version of Pi.single.

Equations

• MulHom.single f i = { toFun := Pi.single i, map_mul' := (_ : ∀ (x₁ x₂ : f i), Pi.single i (x₁ * x₂) = fun j => Pi.single i x₁ j * Pi.single i x₂ j) }

ink

theorem Pi.single_add {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (i : I) (x : f i) (y : f i) : Pi.single i (x + y) = Pi.single i x + Pi.single i y

ink

theorem Pi.mulSingle_mul {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → MulOneClass (f i)] (i : I) (x : f i) (y : f i) : Pi.mulSingle i (x * y) = Pi.mulSingle i x * Pi.mulSingle i y

ink

theorem Pi.single_neg {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → AddGroup (f i)] (i : I) (x : f i) : Pi.single i (-x) = -Pi.single i x

ink

theorem Pi.mulSingle_inv {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → Group (f i)] (i : I) (x : f i) : Pi.mulSingle i x⁻¹ = (Pi.mulSingle i x)⁻¹

ink

theorem Pi.single_sub {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → AddGroup (f i)] (i : I) (x : f i) (y : f i) : Pi.single i (x - y) = Pi.single i x - Pi.single i y

ink

theorem Pi.single_div {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → Group (f i)] (i : I) (x : f i) (y : f i) : Pi.mulSingle i (x / y) = Pi.mulSingle i x / Pi.mulSingle i y

ink

theorem Pi.single_mul {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → MulZeroClass (f i)] (i : I) (x : f i) (y : f i) : Pi.single i (x * y) = Pi.single i x * Pi.single i y

ink

theorem Pi.single_commute {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] : Pairwise fun i j => ∀ (x : f i) (y : f j), AddCommute (Pi.single i x) (Pi.single j y)

The injection into an additive pi group at different indices commutes.

For injections of commuting elements at the same index, see AddCommute.map

ink

theorem Pi.mulSingle_commute {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → MulOneClass (f i)] : Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (Pi.mulSingle i x) (Pi.mulSingle j y)

The injection into a pi group at different indices commutes.

For injections of commuting elements at the same index, see Commute.map

ink

theorem Pi.single_apply_commute {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → AddZeroClass (f i)] (x : (i : I) → f i) (i : I) (j : I) : AddCommute (Pi.single i (x i)) (Pi.single j (x j))

The injection into an additive pi group with the same values commutes.

ink

theorem Pi.mulSingle_apply_commute {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst : (i : I) → MulOneClass (f i)] (x : (i : I) → f i) (i : I) (j : I) : Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))

The injection into a pi group with the same values commutes.

ink

theorem Pi.update_eq_sub_add_single {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst : (i : I) → AddGroup (f i)] (g : (i : I) → f i) (x : f i) : Function.update g i x = g - Pi.single i (g i) + Pi.single i x

ink

theorem Pi.update_eq_div_mul_mulSingle {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst : (i : I) → Group (f i)] (g : (i : I) → f i) (x : f i) : Function.update g i x = g / Pi.mulSingle i (g i) * Pi.mulSingle i x

ink

theorem Pi.single_add_single_eq_single_add_single {I : Type u} [inst : DecidableEq I] {M : Type u_1} [inst : AddCommMonoid M] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u ≠ 0) (hv : v ≠ 0) : Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

ink

theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {I : Type u} [inst : DecidableEq I] {M : Type u_1} [inst : CommMonoid M] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u ≠ 1) (hv : v ≠ 1) : Pi.mulSingle k u * Pi.mulSingle l v = Pi.mulSingle m u * Pi.mulSingle n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

ink

@[simp]

theorem Function.update_zero {I : Type u} {f : I → Type v} [inst : (i : I) → Zero (f i)] [inst : DecidableEq I] (i : I) : Function.update 0 i 0 = 0

ink

@[simp]

theorem Function.update_one {I : Type u} {f : I → Type v} [inst : (i : I) → One (f i)] [inst : DecidableEq I] (i : I) : Function.update 1 i 1 = 1

ink

theorem Function.update_add {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) : Function.update (f₁ + f₂) i (x₁ + x₂) = Function.update f₁ i x₁ + Function.update f₂ i x₂

ink

theorem Function.update_mul {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) : Function.update (f₁ * f₂) i (x₁ * x₂) = Function.update f₁ i x₁ * Function.update f₂ i x₂

ink

theorem Function.update_neg {I : Type u} {f : I → Type v} [inst : (i : I) → Neg (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) : Function.update (-f₁) i (-x₁) = -Function.update f₁ i x₁

ink

theorem Function.update_inv {I : Type u} {f : I → Type v} [inst : (i : I) → Inv (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) : Function.update f₁⁻¹ i x₁⁻¹ = (Function.update f₁ i x₁)⁻¹

ink

theorem Function.update_sub {I : Type u} {f : I → Type v} [inst : (i : I) → Sub (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) : Function.update (f₁ - f₂) i (x₁ - x₂) = Function.update f₁ i x₁ - Function.update f₂ i x₂

ink

theorem Function.update_div {I : Type u} {f : I → Type v} [inst : (i : I) → Div (f i)] [inst : DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) : Function.update (f₁ / f₂) i (x₁ / x₂) = Function.update f₁ i x₁ / Function.update f₂ i x₂

ink

@[simp]

theorem Function.const_eq_zero {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : Nonempty ι] {a : α} : Function.const ι a = 0 ↔ a = 0

ink

@[simp]

theorem Function.const_eq_one {ι : Type u_1} {α : Type u_2} [inst : One α] [inst : Nonempty ι] {a : α} : Function.const ι a = 1 ↔ a = 1

ink

theorem Function.const_ne_zero {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : Nonempty ι] {a : α} : Function.const ι a ≠ 0 ↔ a ≠ 0

ink

theorem Function.const_ne_one {ι : Type u_1} {α : Type u_2} [inst : One α] [inst : Nonempty ι] {a : α} : Function.const ι a ≠ 1 ↔ a ≠ 1

ink

theorem Set.piecewise_add {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) : Set.piecewise s (f₁ + f₂) (g₁ + g₂) = Set.piecewise s f₁ g₁ + Set.piecewise s f₂ g₂

ink

theorem Set.piecewise_mul {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) : Set.piecewise s (f₁ * f₂) (g₁ * g₂) = Set.piecewise s f₁ g₁ * Set.piecewise s f₂ g₂

ink

theorem Set.piecewise_neg {I : Type u} {f : I → Type v} [inst : (i : I) → Neg (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) : Set.piecewise s (-f₁) (-g₁) = -Set.piecewise s f₁ g₁

ink

theorem Set.piecewise_inv {I : Type u} {f : I → Type v} [inst : (i : I) → Inv (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) : Set.piecewise s f₁⁻¹ g₁⁻¹ = (Set.piecewise s f₁ g₁)⁻¹

ink

theorem Set.piecewise_sub {I : Type u} {f : I → Type v} [inst : (i : I) → Sub (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) : Set.piecewise s (f₁ - f₂) (g₁ - g₂) = Set.piecewise s f₁ g₁ - Set.piecewise s f₂ g₂

ink

theorem Set.piecewise_div {I : Type u} {f : I → Type v} [inst : (i : I) → Div (f i)] (s : Set I) [inst : (i : I) → Decidable (i ∈ s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) : Set.piecewise s (f₁ / f₂) (g₁ / g₂) = Set.piecewise s f₁ g₁ / Set.piecewise s f₂ g₂

ink

noncomputable def Function.ExtendByZero.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : AddZeroClass R] : (ι → R) →+ η → R

Function.extend s f 0 as a bundled hom.

Equations

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

ink

def Function.ExtendByZero.hom.proof_1 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ι → η) [inst : AddZeroClass R] : Function.extend s 0 0 = 0

Equations

• (_ : Function.extend s 0 0 = 0) = (_ : Function.extend s 0 0 = 0)

ink

def Function.ExtendByZero.hom.proof_2 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ι → η) [inst : AddZeroClass R] (f : ι → R) (g : ι → R) : ZeroHom.toFun { toFun := fun f => Function.extend s f 0, map_zero' := (_ : Function.extend s 0 0 = 0) } (f + g) = ZeroHom.toFun { toFun := fun f => Function.extend s f 0, map_zero' := (_ : Function.extend s 0 0 = 0) } f + ZeroHom.toFun { toFun := fun f => Function.extend s f 0, map_zero' := (_ : Function.extend s 0 0 = 0) } g

Equations

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

ink

@[simp]

theorem Function.ExtendByOne.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : MulOneClass R] (f : ι → R) : ∀ (a : η), ↑(Function.ExtendByOne.hom R s) f a = Function.extend s f 1 a

ink

@[simp]

theorem Function.ExtendByZero.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : AddZeroClass R] (f : ι → R) : ∀ (a : η), ↑(Function.ExtendByZero.hom R s) f a = Function.extend s f 0 a

ink

noncomputable def Function.ExtendByOne.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : MulOneClass R] : (ι → R) →* η → R

Function.extend s f 1 as a bundled hom.

Equations

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