Extra lemmas about products of monoids and groups

This file proves lemmas about the instances defined in Algebra.Group.Pi.Basic that require more imports.

@[simp]

theorem Set.range_one {α : Type u_5} {β : Type u_6} [One β] [Nonempty α] : range 1 = {1}

@[simp]

theorem Set.range_zero {α : Type u_5} {β : Type u_6} [Zero β] [Nonempty α] : range 0 = {0}

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

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

instance Pi.instIsMulTorsionFree {ι : Type u_1} {M : ι → Type u_3} [(i : ι) → Monoid (M i)] [∀ (i : ι), IsMulTorsionFree (M i)] : IsMulTorsionFree ((i : ι) → M i)

instance Pi.instIsAddTorsionFree {ι : Type u_1} {M : ι → Type u_3} [(i : ι) → AddMonoid (M i)] [∀ (i : ι), IsAddTorsionFree (M i)] : IsAddTorsionFree ((i : ι) → M i)

theorem Pi.one_mono {α : Type u_5} {β : Type u_6} [Preorder α] [Preorder β] [One β] : Monotone 1

theorem Pi.zero_mono {α : Type u_5} {β : Type u_6} [Preorder α] [Preorder β] [Zero β] : Monotone 0

theorem Pi.one_anti {α : Type u_5} {β : Type u_6} [Preorder α] [Preorder β] [One β] : Antitone 1

theorem Pi.zero_anti {α : Type u_5} {β : Type u_6} [Preorder α] [Preorder β] [Zero β] : Antitone 0

theorem MulHom.coe_mul {M : Type u_5} {N : Type u_6} {x✝ : Mul M} {x✝¹ : CommSemigroup N} (f g : M →ₙ* N) : ⇑f * ⇑g = fun (x : M) => f x * g x

theorem AddHom.coe_add {M : Type u_5} {N : Type u_6} {x✝ : Add M} {x✝¹ : AddCommSemigroup N} (f g : M →ₙ+ N) : ⇑f + ⇑g = fun (x : M) => f x + g x

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

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

Equations

• MulHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_mul' := ⋯ }

def AddHom.pi {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {γ : Type w} [Add γ] (g : (i : I) → γ →ₙ+ f i) : γ →ₙ+ (i : I) → f i

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

Equations

• AddHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_add' := ⋯ }

@[simp]

theorem MulHom.pi_apply {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {γ : Type w} [Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[simp]

theorem AddHom.pi_apply {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {γ : Type w} [Add γ] (g : (i : I) → γ →ₙ+ f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[deprecated MulHom.pi (since := "2026-05-29")]

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

Alias of AddHom.pi.

---

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

Equations

• @Pi.addHom = @AddHom.pi

@[deprecated MulHom.pi (since := "2026-05-29")]

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

Alias of MulHom.pi.

---

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

Equations

• @Pi.mulHom = @MulHom.pi

@[deprecated MulHom.pi_apply (since := "2026-05-29")]

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

Alias of AddHom.pi_apply.

@[deprecated MulHom.pi_apply (since := "2026-05-29")]

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

Alias of MulHom.pi_apply.

theorem MulHom.pi_injective {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {γ : Type w} [Nonempty I] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

theorem AddHom.pi_injective {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {γ : Type w} [Nonempty I] [Add γ] (g : (i : I) → γ →ₙ+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

theorem AddHom.injective_pi {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {γ : Type w} [Nonempty I] [Add γ] (g : (i : I) → γ →ₙ+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of AddHom.pi_injective.

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

theorem MulHom.injective_pi {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {γ : Type w} [Nonempty I] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of MulHom.pi_injective.

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

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

Alias of AddHom.pi_injective.

---

Alias of AddHom.pi_injective.

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

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

Alias of MulHom.pi_injective.

def Pi.evalMulHom {I : Type u} (f : I → Type v) [(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 : (i : I) → f i) => g i, map_mul' := ⋯ }

def Pi.evalAddHom {I : Type u} (f : I → Type v) [(i : I) → Add (f i)] (i : I) : ((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 : (i : I) → f i) => g i, map_add' := ⋯ }

@[simp]

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

@[simp]

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

def MulHom.piMap {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → Mul (M i)] [(i : ι) → Mul (N i)] (g : (i : ι) → M i →ₙ* N i) : ((i : ι) → M i) →ₙ* (i : ι) → N i

A family of MulHom's f i : M i →ₙ* N i defines a MulHom MulHom.piMap f : (Π i, M i) →ₙ* (Π i, N i) given by MulHom.piMap f x i = f i x. This is Pi.map for MulHoms.

Equations

• MulHom.piMap g = MulHom.pi fun (i : ι) => (g i).comp (Pi.evalMulHom M i)

def AddHom.piMap {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → Add (M i)] [(i : ι) → Add (N i)] (g : (i : ι) → M i →ₙ+ N i) : ((i : ι) → M i) →ₙ+ (i : ι) → N i

A family of AddHom's f i : M i →ₙ+ N i defines an AddHom AddHom.piMap f : (Π i, M i) →ₙ+ (Π i, N i) given by AddHom.piMap f x i = f i x. This is Pi.map for AddHoms.

Equations

• AddHom.piMap g = AddHom.pi fun (i : ι) => (g i).comp (Pi.evalAddHom M i)

@[simp]

theorem AddHom.piMap_apply {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → Add (M i)] [(i : ι) → Add (N i)] (g : (i : ι) → M i →ₙ+ N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

@[simp]

theorem MulHom.piMap_apply {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → Mul (M i)] [(i : ι) → Mul (N i)] (g : (i : ι) → M i →ₙ* N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

def Pi.constMulHom (α : Type u_5) (β : Type u_6) [Mul β] : β →ₙ* α → β

Function.const as a MulHom.

Equations

• Pi.constMulHom α β = { toFun := Function.const α, map_mul' := ⋯ }

def Pi.constAddHom (α : Type u_5) (β : Type u_6) [Add β] : β →ₙ+ α → β

Function.const as an AddHom.

Equations

• Pi.constAddHom α β = { toFun := Function.const α, map_add' := ⋯ }

@[simp]

theorem Pi.constAddHom_apply (α : Type u_5) (β : Type u_6) [Add β] (a : β) (a✝ : α) : (constAddHom α β) a a✝ = Function.const α a a✝

@[simp]

theorem Pi.constMulHom_apply (α : Type u_5) (β : Type u_6) [Mul β] (a : β) (a✝ : α) : (constMulHom α β) a a✝ = Function.const α a a✝

def MulHom.coeFn (α : Type u_5) (β : Type u_6) [Mul α] [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' := ⋯ }

def AddHom.coeFn (α : Type u_5) (β : Type u_6) [Add α] [AddCommSemigroup β] : (α →ₙ+ β) →ₙ+ α → β

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

See also AddHom.eval.

Equations

• AddHom.coeFn α β = { toFun := fun (g : α →ₙ+ β) => ⇑g, map_add' := ⋯ }

@[simp]

theorem AddHom.coeFn_apply (α : Type u_5) (β : Type u_6) [Add α] [AddCommSemigroup β] (g : α →ₙ+ β) (a : α) : (coeFn α β) g a = g a

@[simp]

theorem MulHom.coeFn_apply (α : Type u_5) (β : Type u_6) [Mul α] [CommSemigroup β] (g : α →ₙ* β) (a : α) : (coeFn α β) g a = g a

def MulHom.compLeft {α : Type u_5} {β : Type u_6} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_7) : (I → α) →ₙ* I → β

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

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_mul' := ⋯ }

def AddHom.compLeft {α : Type u_5} {β : Type u_6} [Add α] [Add β] (f : α →ₙ+ β) (I : Type u_7) : (I → α) →ₙ+ I → β

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

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_add' := ⋯ }

@[simp]

theorem AddHom.compLeft_apply {α : Type u_5} {β : Type u_6} [Add α] [Add β] (f : α →ₙ+ β) (I : Type u_7) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

@[simp]

theorem MulHom.compLeft_apply {α : Type u_5} {β : Type u_6} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_7) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

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

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

Equations

• MonoidHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_one' := ⋯, map_mul' := ⋯ }

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

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

Equations

• AddMonoidHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidHom.pi_apply {I : Type u} {f : I → Type v} [(i : I) → MulOneClass (f i)] {γ : Type w} [MulOneClass γ] (g : (i : I) → γ →* f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[simp]

theorem AddMonoidHom.pi_apply {I : Type u} {f : I → Type v} [(i : I) → AddZeroClass (f i)] {γ : Type w} [AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[deprecated MonoidHom.pi (since := "2026-05-29")]

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

Alias of AddMonoidHom.pi.

---

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

Equations

• @Pi.addMonoidHom = @AddMonoidHom.pi

@[deprecated MonoidHom.pi (since := "2026-05-29")]

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

Alias of MonoidHom.pi.

---

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

Equations

• @Pi.monoidHom = @MonoidHom.pi

@[deprecated MonoidHom.pi_apply (since := "2026-05-29")]

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

Alias of AddMonoidHom.pi_apply.

@[deprecated MonoidHom.pi_apply (since := "2026-05-29")]

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

Alias of MonoidHom.pi_apply.

theorem MonoidHom.pi_injective {I : Type u} {f : I → Type v} [(i : I) → MulOneClass (f i)] {γ : Type w} [Nonempty I] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

theorem AddMonoidHom.pi_injective {I : Type u} {f : I → Type v} [(i : I) → AddZeroClass (f i)] {γ : Type w} [Nonempty I] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

theorem AddMonoidHom.injective_pi {I : Type u} {f : I → Type v} [(i : I) → AddZeroClass (f i)] {γ : Type w} [Nonempty I] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of AddMonoidHom.pi_injective.

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

theorem MonoidHom.injective_pi {I : Type u} {f : I → Type v} [(i : I) → MulOneClass (f i)] {γ : Type w} [Nonempty I] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of MonoidHom.pi_injective.

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

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

Alias of AddMonoidHom.pi_injective.

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

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

Alias of MonoidHom.pi_injective.

def Pi.evalMonoidHom {I : Type u} (f : I → Type v) [(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

• Pi.evalMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_one' := ⋯, map_mul' := ⋯ }

def Pi.evalAddMonoidHom {I : Type u} (f : I → Type v) [(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

• Pi.evalAddMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Pi.coe_evalMonoidHom {I : Type u} (f : I → Type v) [(i : I) → MulOneClass (f i)] (i : I) : ⇑(evalMonoidHom f i) = Function.eval i

def MonoidHom.piMap {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → MulOneClass (M i)] [(i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i) : ((i : ι) → M i) →* (i : ι) → N i

A family of monoid homomorphisms f i : M i →* N i defines a monoid homomorphism MonoidHom.piMap f : (Π i, M i) →* (Π i, N i) given by MonoidHom.piMap f x i = f i x. This is Pi.map for MonoidHoms.

Equations

• MonoidHom.piMap g = MonoidHom.pi fun (i : ι) => (g i).comp (Pi.evalMonoidHom M i)

def AddMonoidHom.piMap {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → AddZeroClass (M i)] [(i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i) : ((i : ι) → M i) →+ (i : ι) → N i

A family of additive monoid homomorphisms f i : M i →+ N i defines an additive monoid homomorphism AddMonoidHom.piMap f : (Π i, M i) →+ (Π i, N i) given by AddMonoidHom.piMap f x i = f i x. This is Pi.map for AddMonoidHoms.

Equations

• AddMonoidHom.piMap g = AddMonoidHom.pi fun (i : ι) => (g i).comp (Pi.evalAddMonoidHom M i)

@[simp]

theorem AddMonoidHom.piMap_apply {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → AddZeroClass (M i)] [(i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

@[simp]

theorem MonoidHom.piMap_apply {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → MulOneClass (M i)] [(i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

def Pi.constMonoidHom (α : Type u_5) (β : Type u_6) [MulOneClass β] : β →* α → β

Function.const as a MonoidHom.

Equations

• Pi.constMonoidHom α β = { toFun := Function.const α, map_one' := ⋯, map_mul' := ⋯ }

def Pi.constAddMonoidHom (α : Type u_5) (β : Type u_6) [AddZeroClass β] : β →+ α → β

Function.const as an AddMonoidHom.

Equations

• Pi.constAddMonoidHom α β = { toFun := Function.const α, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Pi.constAddMonoidHom_apply (α : Type u_5) (β : Type u_6) [AddZeroClass β] (a : β) (a✝ : α) : (constAddMonoidHom α β) a a✝ = Function.const α a a✝

@[simp]

theorem Pi.constMonoidHom_apply (α : Type u_5) (β : Type u_6) [MulOneClass β] (a : β) (a✝ : α) : (constMonoidHom α β) a a✝ = Function.const α a a✝

def MonoidHom.coeFn (α : Type u_5) (β : Type u_6) [MulOneClass α] [CommMonoid β] : (α →* β) →* α → β

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

See also MonoidHom.eval.

Equations

• MonoidHom.coeFn α β = { toFun := fun (g : α →* β) => ⇑g, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.coeFn (α : Type u_5) (β : Type u_6) [AddZeroClass α] [AddCommMonoid β] : (α →+ β) →+ α → β

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

See also AddMonoidHom.eval.

Equations

• AddMonoidHom.coeFn α β = { toFun := fun (g : α →+ β) => ⇑g, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.coeFn_apply (α : Type u_5) (β : Type u_6) [AddZeroClass α] [AddCommMonoid β] (g : α →+ β) (a : α) : (coeFn α β) g a = g a

@[simp]

theorem MonoidHom.coeFn_apply (α : Type u_5) (β : Type u_6) [MulOneClass α] [CommMonoid β] (g : α →* β) (a : α) : (coeFn α β) g a = g a

def MonoidHom.compLeft {α : Type u_5} {β : Type u_6} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_7) : (I → α) →* I → β

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

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.compLeft {α : Type u_5} {β : Type u_6} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_7) : (I → α) →+ I → β

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

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.compLeft_apply {α : Type u_5} {β : Type u_6} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_7) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

@[simp]

theorem MonoidHom.compLeft_apply {α : Type u_5} {β : Type u_6} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_7) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

def OneHom.mulSingle {I : Type u} (f : I → Type v) [DecidableEq I] [(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.mulSingle f i = { toFun := Pi.mulSingle i, map_one' := ⋯ }

def ZeroHom.single {I : Type u} (f : I → Type v) [DecidableEq I] [(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' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem OneHom.coe_mulSingle {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → One (f i)] (i : I) : ⇑(mulSingle f i) = Pi.mulSingle i

@[simp]

theorem ZeroHom.coe_single {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → Zero (f i)] (i : I) : ⇑(single f i) = Pi.single i

def MonoidHom.mulSingle {I : Type u} (f : I → Type v) [DecidableEq I] [(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

• MonoidHom.mulSingle f i = { toOneHom := OneHom.mulSingle f i, map_mul' := ⋯ }

def AddMonoidHom.single {I : Type u} (f : I → Type v) [DecidableEq I] [(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

• AddMonoidHom.single f i = { toZeroHom := ZeroHom.single f i, map_add' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidHom.coe_mulSingle {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → MulOneClass (f i)] (i : I) : ⇑(mulSingle f i) = Pi.mulSingle i

@[simp]

theorem AddMonoidHom.coe_single {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → AddZeroClass (f i)] (i : I) : ⇑(single f i) = Pi.single i

theorem Pi.mulSingle_sup {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → SemilatticeSup (f i)] [(i : I) → One (f i)] (i : I) (x y : f i) : mulSingle i (x ⊔ y) = mulSingle i x ⊔ mulSingle i y

theorem Pi.single_sup {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → SemilatticeSup (f i)] [(i : I) → Zero (f i)] (i : I) (x y : f i) : single i (x ⊔ y) = single i x ⊔ single i y

theorem Pi.mulSingle_inf {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → SemilatticeInf (f i)] [(i : I) → One (f i)] (i : I) (x y : f i) : mulSingle i (x ⊓ y) = mulSingle i x ⊓ mulSingle i y

theorem Pi.single_inf {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → SemilatticeInf (f i)] [(i : I) → Zero (f i)] (i : I) (x y : f i) : single i (x ⊓ y) = single i x ⊓ single i y

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

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

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

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

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

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

theorem Pi.mulSingle_pow {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → Monoid (f i)] (i : I) (x : f i) (n : ℕ) : mulSingle i (x ^ n) = mulSingle i x ^ n

theorem Pi.single_nsmul {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → AddMonoid (f i)] (i : I) (x : f i) (n : ℕ) : single i (n • x) = n • single i x

theorem Pi.mulSingle_zpow {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → Group (f i)] (i : I) (x : f i) (n : ℤ) : mulSingle i (x ^ n) = mulSingle i x ^ n

theorem Pi.single_zsmul {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → AddGroup (f i)] (i : I) (x : f i) (n : ℤ) : single i (n • x) = n • single i x

theorem Pi.mulSingle_commute {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → MulOneClass (f i)] : Pairwise fun (i j : I) => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (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

theorem Pi.single_addCommute {I : Type u} {f : I → Type v} [DecidableEq I] [(i : I) → AddZeroClass (f i)] : Pairwise fun (i j : I) => ∀ (x : f i) (y : f j), AddCommute (single i x) (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

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

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

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

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

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

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

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

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

theorem SemiconjBy.pi {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {x y z : (i : I) → f i} (h : ∀ (i : I), SemiconjBy (x i) (y i) (z i)) : SemiconjBy x y z

theorem AddSemiconjBy.pi {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {x y z : (i : I) → f i} (h : ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)) : AddSemiconjBy x y z

theorem Pi.semiconjBy_iff {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {x y z : (i : I) → f i} : SemiconjBy x y z ↔ ∀ (i : I), SemiconjBy (x i) (y i) (z i)

theorem Pi.addSemiconjBy_iff {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {x y z : (i : I) → f i} : AddSemiconjBy x y z ↔ ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)

theorem Commute.pi {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {x y : (i : I) → f i} (h : ∀ (i : I), Commute (x i) (y i)) : Commute x y

theorem AddCommute.pi {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {x y : (i : I) → f i} (h : ∀ (i : I), AddCommute (x i) (y i)) : AddCommute x y

theorem Pi.commute_iff {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] {x y : (i : I) → f i} : Commute x y ↔ ∀ (i : I), Commute (x i) (y i)

theorem Pi.addCommute_iff {I : Type u} {f : I → Type v} [(i : I) → Add (f i)] {x y : (i : I) → f i} : AddCommute x y ↔ ∀ (i : I), AddCommute (x i) (y i)

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

Function.extend s f 1 as a bundled hom.

Equations

• Function.ExtendByOne.hom R s = { toFun := fun (f : ι → R) => Function.extend s f 1, map_one' := ⋯, map_mul' := ⋯ }

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

Function.extend s f 0 as a bundled hom.

Equations

• Function.ExtendByZero.hom R s = { toFun := fun (f : ι → R) => Function.extend s f 0, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

theorem Pi.mulSingle_mono {I : Type u} {f : I → Type v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] : Monotone (mulSingle i)

theorem Pi.single_mono {I : Type u} {f : I → Type v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] : Monotone (single i)

theorem Pi.mulSingle_strictMono {I : Type u} {f : I → Type v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] : StrictMono (mulSingle i)

theorem Pi.single_strictMono {I : Type u} {f : I → Type v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] : StrictMono (single i)

theorem Pi.mulSingle_comp_equiv {α : Type u_2} {m : Type u_5} {n : Type u_6} [DecidableEq n] [DecidableEq m] [One α] (σ : n ≃ m) (i : m) (x : α) : mulSingle i x ∘ ⇑σ = mulSingle (σ.symm i) x

theorem Pi.single_comp_equiv {α : Type u_2} {m : Type u_5} {n : Type u_6} [DecidableEq n] [DecidableEq m] [Zero α] (σ : n ≃ m) (i : m) (x : α) : single i x ∘ ⇑σ = single (σ.symm i) x

@[simp]

theorem Sigma.curry_one {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → One (γ a b)] : curry 1 = 1

@[simp]

theorem Sigma.curry_zero {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Zero (γ a b)] : curry 0 = 0

@[simp]

theorem Sigma.uncurry_one {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → One (γ a b)] : uncurry 1 = 1

@[simp]

theorem Sigma.uncurry_zero {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Zero (γ a b)] : uncurry 0 = 0

@[simp]

theorem Sigma.curry_mul {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Mul (γ a b)] (x y : (i : (a : α) × β a) → γ i.fst i.snd) : curry (x * y) = curry x * curry y

@[simp]

theorem Sigma.curry_add {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Add (γ a b)] (x y : (i : (a : α) × β a) → γ i.fst i.snd) : curry (x + y) = curry x + curry y

@[simp]

theorem Sigma.uncurry_mul {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Mul (γ a b)] (x y : (a : α) → (b : β a) → γ a b) : uncurry (x * y) = uncurry x * uncurry y

@[simp]

theorem Sigma.uncurry_add {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Add (γ a b)] (x y : (a : α) → (b : β a) → γ a b) : uncurry (x + y) = uncurry x + uncurry y

@[simp]

theorem Sigma.curry_inv {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Inv (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) : curry x⁻¹ = (curry x)⁻¹

@[simp]

theorem Sigma.curry_neg {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Neg (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) : curry (-x) = -curry x

@[simp]

theorem Sigma.uncurry_inv {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Inv (γ a b)] (x : (a : α) → (b : β a) → γ a b) : uncurry x⁻¹ = (uncurry x)⁻¹

@[simp]

theorem Sigma.uncurry_neg {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [(a : α) → (b : β a) → Neg (γ a b)] (x : (a : α) → (b : β a) → γ a b) : uncurry (-x) = -uncurry x

@[simp]

theorem Sigma.curry_mulSingle {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → One (γ a b)] (i : (a : α) × β a) (x : γ i.fst i.snd) : curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)

@[simp]

theorem Sigma.curry_single {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → Zero (γ a b)] (i : (a : α) × β a) (x : γ i.fst i.snd) : curry (Pi.single i x) = Pi.single i.fst (Pi.single i.snd x)

@[simp]

theorem Sigma.uncurry_mulSingle_mulSingle {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → One (γ a b)] (a : α) (b : β a) (x : γ a b) : uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x

@[simp]

theorem Sigma.uncurry_single_single {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → Zero (γ a b)] (a : α) (b : β a) (x : γ a b) : uncurry (Pi.single a (Pi.single b x)) = Pi.single ⟨a, b⟩ x