# Documentation

Mathlib.Algebra.Group.Pi

# Pi instances for groups and monoids #

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

theorem Set.preimage_zero {α : Type u_3} {β : Type u_4} [Zero β] (s : Set β) [Decidable (0 s)] :
0 ⁻¹' s = if 0 s then Set.univ else
theorem Set.preimage_one {α : Type u_3} {β : Type u_4} [One β] (s : Set β) [Decidable (1 s)] :
1 ⁻¹' s = if 1 s then Set.univ else
instance Pi.addSemigroup {I : Type u} {f : IType v} [(i : I) → AddSemigroup (f i)] :
AddSemigroup ((i : I) → f i)
theorem Pi.addSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddSemigroup (f i)] :
∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)
instance Pi.semigroup {I : Type u} {f : IType v} [(i : I) → Semigroup (f i)] :
Semigroup ((i : I) → f i)
instance Pi.addCommSemigroup {I : Type u} {f : IType v} [(i : I) → AddCommSemigroup (f i)] :
AddCommSemigroup ((i : I) → f i)
theorem Pi.addCommSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(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)
theorem Pi.addCommSemigroup.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommSemigroup (f i)] :
∀ (a b : (i : I) → f i), a + b = b + a
instance Pi.commSemigroup {I : Type u} {f : IType v} [(i : I) → CommSemigroup (f i)] :
CommSemigroup ((i : I) → f i)
theorem Pi.addZeroClass.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddZeroClass (f i)] :
∀ (a : (i : I) → f i), a + 0 = a
instance Pi.addZeroClass {I : Type u} {f : IType v} [(i : I) → AddZeroClass (f i)] :
AddZeroClass ((i : I) → f i)
theorem Pi.addZeroClass.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddZeroClass (f i)] :
∀ (a : (i : I) → f i), 0 + a = a
instance Pi.mulOneClass {I : Type u} {f : IType v} [(i : I) → MulOneClass (f i)] :
MulOneClass ((i : I) → f i)
instance Pi.negZeroClass {I : Type u} {f : IType v} [(i : I) → NegZeroClass (f i)] :
NegZeroClass ((i : I) → f i)
theorem Pi.negZeroClass.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → NegZeroClass (f i)] :
-0 = 0
instance Pi.invOneClass {I : Type u} {f : IType v} [(i : I) → InvOneClass (f i)] :
InvOneClass ((i : I) → f i)
theorem Pi.addMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(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)
theorem Pi.addMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] :
∀ (x : (i : I) → f i), (fun n x i => n x i) 0 x = 0
theorem Pi.addMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
theorem Pi.addMonoid.proof_5 {I : Type u_1} {f : IType u_2} [(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
instance Pi.addMonoid {I : Type u} {f : IType v} [(i : I) → AddMonoid (f i)] :
AddMonoid ((i : I) → f i)
instance Pi.monoid {I : Type u} {f : IType v} [(i : I) → Monoid (f i)] :
Monoid ((i : I) → f i)
instance Pi.addMonoidWithOne {I : Type u} {f : IType v} [(i : I) → AddMonoidWithOne (f i)] :
AddMonoidWithOne ((i : I) → f i)
theorem Pi.addCommMonoid.proof_5 {I : Type u_2} {f : IType u_1} [(i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
theorem Pi.addCommMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommMonoid (f i)] (x : (i : I) → f i) :
= 0
theorem Pi.addCommMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = x +
theorem Pi.addCommMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addCommMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
instance Pi.addCommMonoid {I : Type u} {f : IType v} [(i : I) → AddCommMonoid (f i)] :
AddCommMonoid ((i : I) → f i)
instance Pi.commMonoid {I : Type u} {f : IType v} [(i : I) → CommMonoid (f i)] :
CommMonoid ((i : I) → f i)
theorem Pi.subNegMonoid.proof_7 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (n : ) (a : (i : I) → f i), (fun z x i => z x i) () a = a + (fun z x i => z x i) () a
theorem Pi.subNegMonoid.proof_8 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (n : ) (a : (i : I) → f i), (fun z x i => z x i) () a = -(fun z x i => z x i) (↑()) a
theorem Pi.subNegMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = x +
theorem Pi.subNegMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] (x : (i : I) → f i) :
= 0
instance Pi.subNegMonoid {I : Type u} {f : IType v} [(i : I) → SubNegMonoid (f i)] :
SubNegMonoid ((i : I) → f i)
theorem Pi.subNegMonoid.proof_6 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (a : (i : I) → f i), (fun z x i => z x i) 0 a = 0
theorem Pi.subNegMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
theorem Pi.subNegMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.subNegMonoid.proof_5 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (a b : (i : I) → f i), a - b = a + -b
instance Pi.divInvMonoid {I : Type u} {f : IType v} [(i : I) → DivInvMonoid (f i)] :
DivInvMonoid ((i : I) → f i)
instance Pi.subNegZeroMonoid {I : Type u} {f : IType v} [(i : I) → SubNegZeroMonoid (f i)] :
SubNegZeroMonoid ((i : I) → f i)
theorem Pi.subNegZeroMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] (n : ) (a : (i : I) → f i) :
= a +
theorem Pi.subNegZeroMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] (a : (i : I) → f i) :
= 0
theorem Pi.subNegZeroMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a - b = a + -b
theorem Pi.subNegZeroMonoid.proof_5 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] :
-0 = 0
theorem Pi.subNegZeroMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] (n : ) (a : (i : I) → f i) :
instance Pi.divInvOneMonoid {I : Type u} {f : IType v} [(i : I) → DivInvOneMonoid (f i)] :
DivInvOneMonoid ((i : I) → f i)
instance Pi.involutiveNeg {I : Type u} {f : IType v} [(i : I) → InvolutiveNeg (f i)] :
InvolutiveNeg ((i : I) → f i)
theorem Pi.involutiveNeg.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → InvolutiveNeg (f i)] :
∀ (x : (i : I) → f i), - -x = x
instance Pi.involutiveInv {I : Type u} {f : IType v} [(i : I) → InvolutiveInv (f i)] :
InvolutiveInv ((i : I) → f i)
theorem Pi.subtractionMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) :
= 0
theorem Pi.subtractionMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] (n : ) (a : (i : I) → f i) :
theorem Pi.subtractionMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a - b = a + -b
theorem Pi.subtractionMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] (n : ) (a : (i : I) → f i) :
= a +
theorem Pi.subtractionMonoid.proof_7 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] :
∀ (a b : (i : I) → f i), a + b = 0-a = b
theorem Pi.subtractionMonoid.proof_6 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] :
∀ (a b : (i : I) → f i), -(a + b) = -b + -a
theorem Pi.subtractionMonoid.proof_5 {I : Type u_2} {f : IType u_1} [(i : I) → SubtractionMonoid (f i)] (x : (i : I) → f i) :
- -x = x
instance Pi.subtractionMonoid {I : Type u} {f : IType v} [(i : I) → SubtractionMonoid (f i)] :
SubtractionMonoid ((i : I) → f i)
instance Pi.divisionMonoid {I : Type u} {f : IType v} [(i : I) → DivisionMonoid (f i)] :
DivisionMonoid ((i : I) → f i)
theorem Pi.subtractionCommMonoid.proof_4 {I : Type u_2} {f : IType u_1} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
theorem Pi.subtractionCommMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) :
-(a + b) = -b + -a
theorem Pi.subtractionCommMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = 0-a = b
theorem Pi.subtractionCommMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → ] (x : (i : I) → f i) :
- -x = x
instance Pi.subtractionCommMonoid {I : Type u} {f : IType v} [(i : I) → ] :
SubtractionCommMonoid ((i : I) → f i)
instance Pi.instDivisionCommMonoidForAll {I : Type u} {f : IType v} [(i : I) → DivisionCommMonoid (f i)] :
DivisionCommMonoid ((i : I) → f i)
theorem Pi.addGroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a - b = a + -b
theorem Pi.addGroup.proof_5 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] :
∀ (a : (i : I) → f i), -a + a = 0
instance Pi.addGroup {I : Type u} {f : IType v} [(i : I) → AddGroup (f i)] :
AddGroup ((i : I) → f i)
theorem Pi.addGroup.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] (a : (i : I) → f i) :
= 0
theorem Pi.addGroup.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] (n : ) (a : (i : I) → f i) :
= a +
theorem Pi.addGroup.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] (n : ) (a : (i : I) → f i) :
instance Pi.group {I : Type u} {f : IType v} [(i : I) → Group (f i)] :
Group ((i : I) → f i)
instance Pi.addGroupWithOne {I : Type u} {f : IType v} [(i : I) → AddGroupWithOne (f i)] :
AddGroupWithOne ((i : I) → f i)
instance Pi.addCommGroup {I : Type u} {f : IType v} [(i : I) → AddCommGroup (f i)] :
AddCommGroup ((i : I) → f i)
theorem Pi.addCommGroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommGroup (f i)] (a : (i : I) → f i) :
-a + a = 0
theorem Pi.addCommGroup.proof_2 {I : Type u_2} {f : IType u_1} [(i : I) → AddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
instance Pi.commGroup {I : Type u} {f : IType v} [(i : I) → CommGroup (f i)] :
CommGroup ((i : I) → f i)
instance Pi.addLeftCancelSemigroup {I : Type u} {f : IType v} [(i : I) → ] :
AddLeftCancelSemigroup ((i : I) → f i)
theorem Pi.addLeftCancelSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b + c = a + (b + c)
theorem Pi.addLeftCancelSemigroup.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → ] :
∀ (a b c : (i : I) → f i), a + b = a + cb = c
instance Pi.leftCancelSemigroup {I : Type u} {f : IType v} [(i : I) → LeftCancelSemigroup (f i)] :
LeftCancelSemigroup ((i : I) → f i)
instance Pi.addRightCancelSemigroup {I : Type u} {f : IType v} [(i : I) → ] :
AddRightCancelSemigroup ((i : I) → f i)
theorem Pi.addRightCancelSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b + c = a + (b + c)
theorem Pi.addRightCancelSemigroup.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → ] :
∀ (a b c : (i : I) → f i), a + b = c + ba = c
instance Pi.rightCancelSemigroup {I : Type u} {f : IType v} [(i : I) → RightCancelSemigroup (f i)] :
RightCancelSemigroup ((i : I) → f i)
theorem Pi.addLeftCancelMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (x : (i : I) → f i) :
= 0
theorem Pi.addLeftCancelMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addLeftCancelMonoid.proof_5 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = x +
theorem Pi.addLeftCancelMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b = a + cb = c
theorem Pi.addLeftCancelMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
instance Pi.addLeftCancelMonoid {I : Type u} {f : IType v} [(i : I) → AddLeftCancelMonoid (f i)] :
AddLeftCancelMonoid ((i : I) → f i)
instance Pi.leftCancelMonoid {I : Type u} {f : IType v} [(i : I) → LeftCancelMonoid (f i)] :
LeftCancelMonoid ((i : I) → f i)
instance Pi.addRightCancelMonoid {I : Type u} {f : IType v} [(i : I) → AddRightCancelMonoid (f i)] :
AddRightCancelMonoid ((i : I) → f i)
theorem Pi.addRightCancelMonoid.proof_5 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = x +
theorem Pi.addRightCancelMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addRightCancelMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
theorem Pi.addRightCancelMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (x : (i : I) → f i) :
= 0
theorem Pi.addRightCancelMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b = c + ba = c
instance Pi.rightCancelMonoid {I : Type u} {f : IType v} [(i : I) → RightCancelMonoid (f i)] :
RightCancelMonoid ((i : I) → f i)
theorem Pi.addCancelMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelMonoid (f i)] (x : (i : I) → f i) :
theorem Pi.addCancelMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelMonoid (f i)] (n : ) (x : (i : I) → f i) :
instance Pi.addCancelMonoid {I : Type u} {f : IType v} [(i : I) → AddCancelMonoid (f i)] :
AddCancelMonoid ((i : I) → f i)
theorem Pi.addCancelMonoid.proof_5 {I : Type u_2} {f : IType u_1} [(i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b = c + ba = c
theorem Pi.addCancelMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addCancelMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
instance Pi.cancelMonoid {I : Type u} {f : IType v} [(i : I) → CancelMonoid (f i)] :
CancelMonoid ((i : I) → f i)
theorem Pi.addCancelCommMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelCommMonoid (f i)] (n : ) (x : (i : I) → f i) :
theorem Pi.addCancelCommMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
instance Pi.addCancelCommMonoid {I : Type u} {f : IType v} [(i : I) → AddCancelCommMonoid (f i)] :
AddCancelCommMonoid ((i : I) → f i)
theorem Pi.addCancelCommMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addCancelCommMonoid.proof_5 {I : Type u_2} {f : IType u_1} [(i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
theorem Pi.addCancelCommMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddCancelCommMonoid (f i)] (x : (i : I) → f i) :
instance Pi.cancelCommMonoid {I : Type u} {f : IType v} [(i : I) → CancelCommMonoid (f i)] :
CancelCommMonoid ((i : I) → f i)
instance Pi.mulZeroClass {I : Type u} {f : IType v} [(i : I) → MulZeroClass (f i)] :
MulZeroClass ((i : I) → f i)
instance Pi.mulZeroOneClass {I : Type u} {f : IType v} [(i : I) → MulZeroOneClass (f i)] :
MulZeroOneClass ((i : I) → f i)
instance Pi.monoidWithZero {I : Type u} {f : IType v} [(i : I) → MonoidWithZero (f i)] :
MonoidWithZero ((i : I) → f i)
instance Pi.commMonoidWithZero {I : Type u} {f : IType v} [(i : I) → CommMonoidWithZero (f i)] :
CommMonoidWithZero ((i : I) → f i)
instance Pi.semigroupWithZero {I : Type u} {f : IType v} [(i : I) → SemigroupWithZero (f i)] :
SemigroupWithZero ((i : I) → f i)
∀ {x : Add M} {x_1 : } (f g : AddHom M N), f + g = fun x_2 => f x_2 + g x_2
theorem MulHom.coe_mul {M : Type u_3} {N : Type u_4} :
∀ {x : Mul M} {x_1 : } (f g : M →ₙ* N), f * g = fun x_2 => f x_2 * g x_2
def Pi.addHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) :
AddHom γ ((i : I) → f i)

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

Instances For
theorem Pi.addHom.proof_1 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → Add (f i)] [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
@[simp]
theorem Pi.addHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) (x : γ) (i : I) :
↑() x i = ↑(g i) x
@[simp]
theorem Pi.mulHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) :
↑() x i = ↑(g i) x
def Pi.mulHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) :
γ →ₙ* (i : I) → f i

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

Instances For
abbrev Pi.addHom_injective.match_1 {I : Type u_1} (motive : Prop) :
(x : ) → ((i : I) → motive (_ : )) → motive x
Instances For
theorem Pi.addHom_injective {I : Type u} {f : IType v} {γ : Type w} [] [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) (hg : ∀ (i : I), Function.Injective ↑(g i)) :
theorem Pi.mulHom_injective {I : Type u} {f : IType v} {γ : Type w} [] [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) :
def Pi.addMonoidHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → AddZeroClass (f i)] [] (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.

Instances For
theorem Pi.addMonoidHom.proof_2 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → AddZeroClass (f i)] [] (g : (i : I) → γ →+ f i) (x : γ) (y : γ) :
theorem Pi.addMonoidHom.proof_1 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → AddZeroClass (f i)] [] (g : (i : I) → γ →+ f i) :
(fun x i => ↑(g i) x) 0 = 0
@[simp]
theorem Pi.monoidHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → MulOneClass (f i)] [] (g : (i : I) → γ →* f i) (x : γ) (i : I) :
↑() x i = ↑(g i) x
@[simp]
theorem Pi.addMonoidHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → AddZeroClass (f i)] [] (g : (i : I) → γ →+ f i) (x : γ) (i : I) :
↑() x i = ↑(g i) x
def Pi.monoidHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → MulOneClass (f i)] [] (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.

Instances For
theorem Pi.addMonoidHom_injective {I : Type u} {f : IType v} {γ : Type w} [] [(i : I) → AddZeroClass (f i)] [] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) :
theorem Pi.monoidHom_injective {I : Type u} {f : IType v} {γ : Type w} [] [(i : I) → MulOneClass (f i)] [] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) :
theorem Pi.evalAddHom.proof_1 {I : Type u_2} (f : IType u_1) [(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
def Pi.evalAddHom {I : Type u} (f : IType v) [(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.

Instances For
@[simp]
theorem Pi.evalAddHom_apply {I : Type u} (f : IType v) [(i : I) → Add (f i)] (i : I) (g : (i : I) → f i) :
↑() g = g i
@[simp]
theorem Pi.evalMulHom_apply {I : Type u} (f : IType v) [(i : I) → Mul (f i)] (i : I) (g : (i : I) → f i) :
↑() g = g i
def Pi.evalMulHom {I : Type u} (f : IType 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.

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

Function.const as an AddHom.

Instances For
@[simp]
theorem Pi.constAddHom_apply (α : Type u_3) (β : Type u_4) [Add β] (a : β) :
∀ (a : α), ↑() a a =
@[simp]
theorem Pi.constMulHom_apply (α : Type u_3) (β : Type u_4) [Mul β] (a : β) :
∀ (a : α), ↑() a a =
def Pi.constMulHom (α : Type u_3) (β : Type u_4) [Mul β] :
β →ₙ* αβ

Function.const as a MulHom.

Instances For
theorem AddHom.coeFn.proof_1 (α : Type u_2) (β : Type u_1) [Add α] [] :
∀ (x x_1 : AddHom α β), (fun g => g) (x + x_1) = (fun g => g) (x + x_1)
def AddHom.coeFn (α : Type u_3) (β : Type u_4) [Add α] [] :

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

See also AddHom.eval.

Instances For
@[simp]
theorem MulHom.coeFn_apply (α : Type u_3) (β : Type u_4) [Mul α] [] (g : α →ₙ* β) (a : α) :
↑() g a = g a
@[simp]
theorem AddHom.coeFn_apply (α : Type u_3) (β : Type u_4) [Add α] [] (g : AddHom α β) (a : α) :
↑() g a = g a
def MulHom.coeFn (α : Type u_3) (β : Type u_4) [Mul α] [] :
(α →ₙ* β) →ₙ* αβ

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

See also MulHom.eval.

Instances For
theorem AddHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [Add α] [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
def AddHom.compLeft {α : Type u_3} {β : Type u_4} [Add α] [Add β] (f : AddHom α β) (I : Type u_5) :

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

Instances For
@[simp]
theorem MulHom.compLeft_apply {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_5) (h : Iα) :
∀ (a : I), ↑() h a = (f h) a
@[simp]
theorem AddHom.compLeft_apply {α : Type u_3} {β : Type u_4} [Add α] [Add β] (f : AddHom α β) (I : Type u_5) (h : Iα) :
∀ (a : I), ↑() h a = (f h) a
def MulHom.compLeft {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_5) :
(Iα) →ₙ* Iβ

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

Instances For
theorem Pi.evalAddMonoidHom.proof_1 {I : Type u_2} (f : IType u_1) [(i : I) → AddZeroClass (f i)] (i : I) :
OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0
theorem Pi.evalAddMonoidHom.proof_2 {I : Type u_2} (f : IType u_1) [(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
def Pi.evalAddMonoidHom {I : Type u} (f : IType 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.

Instances For
@[simp]
theorem Pi.evalMonoidHom_apply {I : Type u} (f : IType v) [(i : I) → MulOneClass (f i)] (i : I) (g : (i : I) → f i) :
↑() g = g i
@[simp]
theorem Pi.evalAddMonoidHom_apply {I : Type u} (f : IType v) [(i : I) → AddZeroClass (f i)] (i : I) (g : (i : I) → f i) :
↑() g = g i
def Pi.evalMonoidHom {I : Type u} (f : IType 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.

Instances For
theorem Pi.constAddMonoidHom.proof_2 (α : Type u_1) (β : Type u_2) [] :
∀ (x x_1 : β), ZeroHom.toFun { toFun := , map_zero' := (_ : = ) } (x + x_1) = ZeroHom.toFun { toFun := , map_zero' := (_ : = ) } (x + x_1)
def Pi.constAddMonoidHom (α : Type u_3) (β : Type u_4) [] :
β →+ αβ

Function.const as an AddMonoidHom.

Instances For
theorem Pi.constAddMonoidHom.proof_1 (α : Type u_1) (β : Type u_2) [] :
=
@[simp]
theorem Pi.constAddMonoidHom_apply (α : Type u_3) (β : Type u_4) [] (a : β) :
∀ (a : α), ↑() a a =
@[simp]
theorem Pi.constMonoidHom_apply (α : Type u_3) (β : Type u_4) [] (a : β) :
∀ (a : α), ↑() a a =
def Pi.constMonoidHom (α : Type u_3) (β : Type u_4) [] :
β →* αβ

Function.const as a MonoidHom.

Instances For
def AddMonoidHom.coeFn (α : Type u_3) (β : Type u_4) [] [] :
(α →+ β) →+ αβ

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

See also AddMonoidHom.eval.

Instances For
theorem AddMonoidHom.coeFn.proof_2 (α : Type u_2) (β : Type u_1) [] [] :
∀ (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)
theorem AddMonoidHom.coeFn.proof_1 (α : Type u_1) (β : Type u_2) [] [] :
(fun g => g) 0 = (fun g => g) 0
@[simp]
theorem AddMonoidHom.coeFn_apply (α : Type u_3) (β : Type u_4) [] [] (g : α →+ β) (a : α) :
↑() g a = g a
@[simp]
theorem MonoidHom.coeFn_apply (α : Type u_3) (β : Type u_4) [] [] (g : α →* β) (a : α) :
↑() g a = g a
def MonoidHom.coeFn (α : Type u_3) (β : Type u_4) [] [] :
(α →* β) →* αβ

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

See also MonoidHom.eval.

Instances For
def AddMonoidHom.compLeft {α : Type u_3} {β : Type u_4} [] [] (f : α →+ β) (I : Type u_5) :
(Iα) →+ Iβ

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

Instances For
theorem AddMonoidHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [] [] (f : α →+ β) (I : Type u_1) :
(fun h => f h) 0 = 0
theorem AddMonoidHom.compLeft.proof_2 {α : Type u_3} {β : Type u_2} [] [] (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
@[simp]
theorem AddMonoidHom.compLeft_apply {α : Type u_3} {β : Type u_4} [] [] (f : α →+ β) (I : Type u_5) (h : Iα) :
∀ (a : I), ↑() h a = (f h) a
@[simp]
theorem MonoidHom.compLeft_apply {α : Type u_3} {β : Type u_4} [] [] (f : α →* β) (I : Type u_5) (h : Iα) :
∀ (a : I), ↑() h a = (f h) a
def MonoidHom.compLeft {α : Type u_3} {β : Type u_4} [] [] (f : α →* β) (I : Type u_5) :
(Iα) →* Iβ

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

Instances For
def ZeroHom.single {I : Type u} (f : IType v) [] [(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.

Instances For
theorem ZeroHom.single.proof_1 {I : Type u_1} (f : IType u_2) [] [(i : I) → Zero (f i)] (i : I) :
= 0
def OneHom.single {I : Type u} (f : IType v) [] [(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.

Instances For
@[simp]
theorem ZeroHom.single_apply {I : Type u} (f : IType v) [] [(i : I) → Zero (f i)] (i : I) (x : f i) :
↑() x =
@[simp]
theorem OneHom.single_apply {I : Type u} (f : IType v) [] [(i : I) → One (f i)] (i : I) (x : f i) :
↑() x =
theorem AddMonoidHom.single.proof_2 {I : Type u_1} (f : IType u_2) [] [(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
theorem AddMonoidHom.single.proof_1 {I : Type u_1} (f : IType u_2) [] [(i : I) → AddZeroClass (f i)] (i : I) :
def AddMonoidHom.single {I : Type u} (f : IType v) [] [(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.

Instances For
def MonoidHom.single {I : Type u} (f : IType v) [] [(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.

Instances For
@[simp]
theorem AddMonoidHom.single_apply {I : Type u} (f : IType v) [] [(i : I) → AddZeroClass (f i)] (i : I) (x : f i) :
↑() x =
@[simp]
theorem MonoidHom.single_apply {I : Type u} (f : IType v) [] [(i : I) → MulOneClass (f i)] (i : I) (x : f i) :
↑() x =
@[simp]
theorem MulHom.single_apply {I : Type u} (f : IType v) [] [(i : I) → MulZeroClass (f i)] (i : I) (x : f i) (j : I) :
↑() x j = Pi.single i x j
def MulHom.single {I : Type u} (f : IType v) [] [(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.

Instances For
theorem Pi.single_sup {I : Type u} {f : IType v} [] [(i : I) → SemilatticeSup (f i)] [(i : I) → Zero (f i)] (i : I) (x : f i) (y : f i) :
Pi.single i (x y) =
theorem Pi.mulSingle_sup {I : Type u} {f : IType v} [] [(i : I) → SemilatticeSup (f i)] [(i : I) → One (f i)] (i : I) (x : f i) (y : f i) :
theorem Pi.single_inf {I : Type u} {f : IType v} [] [(i : I) → SemilatticeInf (f i)] [(i : I) → Zero (f i)] (i : I) (x : f i) (y : f i) :
Pi.single i (x y) =
theorem Pi.mulSingle_inf {I : Type u} {f : IType v} [] [(i : I) → SemilatticeInf (f i)] [(i : I) → One (f i)] (i : I) (x : f i) (y : f i) :
theorem Pi.single_add {I : Type u} {f : IType v} [] [(i : I) → AddZeroClass (f i)] (i : I) (x : f i) (y : f i) :
Pi.single i (x + y) = +
theorem Pi.mulSingle_mul {I : Type u} {f : IType v} [] [(i : I) → MulOneClass (f i)] (i : I) (x : f i) (y : f i) :
Pi.mulSingle i (x * y) = *
theorem Pi.single_neg {I : Type u} {f : IType v} [] [(i : I) → AddGroup (f i)] (i : I) (x : f i) :
Pi.single i (-x) = -
theorem Pi.mulSingle_inv {I : Type u} {f : IType v} [] [(i : I) → Group (f i)] (i : I) (x : f i) :
= ()⁻¹
theorem Pi.single_sub {I : Type u} {f : IType v} [] [(i : I) → AddGroup (f i)] (i : I) (x : f i) (y : f i) :
Pi.single i (x - y) = -
theorem Pi.single_div {I : Type u} {f : IType v} [] [(i : I) → Group (f i)] (i : I) (x : f i) (y : f i) :
Pi.mulSingle i (x / y) = /
theorem Pi.single_mul {I : Type u} {f : IType v} [] [(i : I) → MulZeroClass (f i)] (i : I) (x : f i) (y : f i) :
Pi.single i (x * y) = *
theorem Pi.single_mul_left_apply {I : Type u} {f : IType v} (x : (i : I) → f i) (i : I) (j : I) [] [(i : I) → MulZeroClass (f i)] (a : f i) :
Pi.single i (a * x i) j = Pi.single i a j * x j
theorem Pi.single_mul_right_apply {I : Type u} {f : IType v} (x : (i : I) → f i) (i : I) (j : I) [] [(i : I) → MulZeroClass (f i)] (a : f i) :
Pi.single i (x i * a) j = x j * Pi.single i a j
theorem Pi.single_mul_left {I : Type u} {f : IType v} (x : (i : I) → f i) (i : I) [] [(i : I) → MulZeroClass (f i)] (a : f i) :
Pi.single i (a * x i) = * x
theorem Pi.single_mul_right {I : Type u} {f : IType v} (x : (i : I) → f i) (i : I) [] [(i : I) → MulZeroClass (f i)] (a : f i) :
Pi.single i (x i * a) = x *
theorem Pi.single_commute {I : Type u} {f : IType v} [] [(i : I) → AddZeroClass (f i)] :
Pairwise fun i j => ∀ (x : f i) (y : f j), AddCommute () ()

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

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_apply_commute {I : Type u} {f : IType v} [] [(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.

theorem Pi.mulSingle_apply_commute {I : Type u} {f : IType v} [] [(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.

theorem Pi.update_eq_sub_add_single {I : Type u} {f : IType v} (i : I) [] [(i : I) → AddGroup (f i)] (g : (i : I) → f i) (x : f i) :
= g - Pi.single i (g i) +
theorem Pi.update_eq_div_mul_mulSingle {I : Type u} {f : IType v} (i : I) [] [(i : I) → Group (f i)] (g : (i : I) → f i) (x : f i) :
= g / Pi.mulSingle i (g i) *
theorem Pi.single_add_single_eq_single_add_single {I : Type u} [] {M : Type u_3} [] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u 0) (hv : v 0) :
+ = + k = m l = n u = v k = n l = m u + v = 0 k = l m = n
theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {I : Type u} [] {M : Type u_3} [] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u 1) (hv : v 1) :
* = * k = m l = n u = v k = n l = m u * v = 1 k = l m = n
@[simp]
theorem Function.update_zero {I : Type u} {f : IType v} [(i : I) → Zero (f i)] [] (i : I) :
= 0
@[simp]
theorem Function.update_one {I : Type u} {f : IType v} [(i : I) → One (f i)] [] (i : I) :
= 1
theorem Function.update_add {I : Type u} {f : IType v} [(i : I) → Add (f 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₂
theorem Function.update_mul {I : Type u} {f : IType v} [(i : I) → Mul (f 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₂
theorem Function.update_neg {I : Type u} {f : IType v} [(i : I) → Neg (f i)] [] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) :
Function.update (-f₁) i (-x₁) = -Function.update f₁ i x₁
theorem Function.update_inv {I : Type u} {f : IType v} [(i : I) → Inv (f i)] [] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) :
theorem Function.update_sub {I : Type u} {f : IType v} [(i : I) → Sub (f 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₂
theorem Function.update_div {I : Type u} {f : IType v} [(i : I) → Div (f 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₂
@[simp]
theorem Function.const_eq_zero {ι : Type u_1} {α : Type u_2} [Zero α] [] {a : α} :
= 0 a = 0
@[simp]
theorem Function.const_eq_one {ι : Type u_1} {α : Type u_2} [One α] [] {a : α} :
= 1 a = 1
theorem Function.const_ne_zero {ι : Type u_1} {α : Type u_2} [Zero α] [] {a : α} :
0 a 0
theorem Function.const_ne_one {ι : Type u_1} {α : Type u_2} [One α] [] {a : α} :
1 a 1
theorem Set.piecewise_add {I : Type u} {f : IType v} [(i : I) → Add (f i)] (s : Set I) [(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₂
theorem Set.piecewise_mul {I : Type u} {f : IType v} [(i : I) → Mul (f i)] (s : Set I) [(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₂
theorem Set.piecewise_neg {I : Type u} {f : IType v} [(i : I) → Neg (f i)] (s : Set I) [(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₁
theorem Set.piecewise_inv {I : Type u} {f : IType v} [(i : I) → Inv (f i)] (s : Set I) [(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₁)⁻¹
theorem Set.piecewise_sub {I : Type u} {f : IType v} [(i : I) → Sub (f i)] (s : Set I) [(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₂
theorem Set.piecewise_div {I : Type u} {f : IType v} [(i : I) → Div (f i)] (s : Set I) [(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₂
noncomputable def Function.ExtendByZero.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [] :
(ιR) →+ ηR

Function.extend s f 0 as a bundled hom.

Instances For
theorem Function.ExtendByZero.hom.proof_1 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ιη) [] :
= 0
theorem Function.ExtendByZero.hom.proof_2 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ιη) [] (f : ιR) (g : ιR) :
ZeroHom.toFun { toFun := fun f => , map_zero' := (_ : = 0) } (f + g) = ZeroHom.toFun { toFun := fun f => , map_zero' := (_ : = 0) } f + ZeroHom.toFun { toFun := fun f => , map_zero' := (_ : = 0) } g
@[simp]
theorem Function.ExtendByOne.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [] (f : ιR) :
∀ (a : η), ↑() f a = Function.extend s f 1 a
@[simp]
theorem Function.ExtendByZero.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [] (f : ιR) :
∀ (a : η), ↑() f a = Function.extend s f 0 a
noncomputable def Function.ExtendByOne.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [] :
(ιR) →* ηR

Function.extend s f 1 as a bundled hom.

Instances For
theorem Pi.single_mono {I : Type u} {f : IType v} (i : I) [] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] :
theorem Pi.mulSingle_mono {I : Type u} {f : IType v} (i : I) [] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] :
theorem Pi.single_strictMono {I : Type u} {f : IType v} (i : I) [] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] :
theorem Pi.mulSingle_strictMono {I : Type u} {f : IType v} (i : I) [] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] :