Pi instances for groups and monoids

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

1, 0, +, *, -, ⁻¹, and / are defined pointwise.

instance PiProp.hasZero {I : Prop} {f : I → Type v} [(i : I) → Zero (f i)] : Zero ((i : I) → f i)

Equations

• PiProp.hasZero = { zero := fun (x : I) => 0 }

instance PiProp.hasOne {I : Prop} {f : I → Type v} [(i : I) → One (f i)] : One ((i : I) → f i)

Equations

• PiProp.hasOne = { one := fun (x : I) => 1 }

instance PiProp.hasAdd {I : Prop} {f : I → Type v} [(i : I) → Add (f i)] : Add ((i : I) → f i)

Equations

• PiProp.hasAdd = { add := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i + g i }

instance PiProp.hasMul {I : Prop} {f : I → Type v} [(i : I) → Mul (f i)] : Mul ((i : I) → f i)

Equations

• PiProp.hasMul = { mul := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i * g i }

instance PiProp.hasNeg {I : Prop} {f : I → Type v} [(i : I) → Neg (f i)] : Neg ((i : I) → f i)

Equations

• PiProp.hasNeg = { neg := fun (f_1 : (i : I) → f i) (i : I) => -f_1 i }

instance PiProp.hasInv {I : Prop} {f : I → Type v} [(i : I) → Inv (f i)] : Inv ((i : I) → f i)

Equations

• PiProp.hasInv = { inv := fun (f_1 : (i : I) → f i) (i : I) => (f_1 i)⁻¹ }

instance PiProp.hasSub {I : Prop} {f : I → Type v} [(i : I) → Sub (f i)] : Sub ((i : I) → f i)

Equations

• PiProp.hasSub = { sub := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i - g i }

instance PiProp.hasDiv {I : Prop} {f : I → Type v} [(i : I) → Div (f i)] : Div ((i : I) → f i)

Equations

• PiProp.hasDiv = { div := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i / g i }

@[simp]

theorem PiProp.zero_apply {I : Prop} {f : I → Type v} [(i : I) → Zero (f i)] (i : I) : 0 i = 0

@[simp]

theorem PiProp.one_apply {I : Prop} {f : I → Type v} [(i : I) → One (f i)] (i : I) : 1 i = 1

instance PiProp.addSemigroup {I : Prop} {f : I → Type v} [(i : I) → AddSemigroup (f i)] : AddSemigroup ((i : I) → f i)

Equations

• PiProp.addSemigroup = AddSemigroup.mk ⋯

theorem PiProp.addSemigroup.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

instance PiProp.semigroup {I : Prop} {f : I → Type v} [(i : I) → Semigroup (f i)] : Semigroup ((i : I) → f i)

Equations

• PiProp.semigroup = Semigroup.mk ⋯

instance PiProp.semigroupWithZero {I : Prop} {f : I → Type v} [(i : I) → SemigroupWithZero (f i)] : SemigroupWithZero ((i : I) → f i)

Equations

• PiProp.semigroupWithZero = let __spread.0 := PiProp.semigroup; SemigroupWithZero.mk ⋯ ⋯

instance PiProp.addCommSemigroup {I : Prop} {f : I → Type v} [(i : I) → AddCommSemigroup (f i)] : AddCommSemigroup ((i : I) → f i)

Equations

• PiProp.addCommSemigroup = let __spread.0 := PiProp.addSemigroup; AddCommSemigroup.mk ⋯

theorem PiProp.addCommSemigroup.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddCommSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

instance PiProp.commSemigroup {I : Prop} {f : I → Type v} [(i : I) → CommSemigroup (f i)] : CommSemigroup ((i : I) → f i)

Equations

• PiProp.commSemigroup = let __spread.0 := PiProp.semigroup; CommSemigroup.mk ⋯

theorem PiProp.addZeroClass.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddZeroClass (f i)] (a : (i : I) → f i) : 0 + a = a

instance PiProp.addZeroClass {I : Prop} {f : I → Type v} [(i : I) → AddZeroClass (f i)] : AddZeroClass ((i : I) → f i)

Equations

• PiProp.addZeroClass = AddZeroClass.mk ⋯ ⋯

theorem PiProp.addZeroClass.proof_2 {I : Prop} {f : I → Type u_1} [(i : I) → AddZeroClass (f i)] (a : (i : I) → f i) : a + 0 = a

instance PiProp.mulOneClass {I : Prop} {f : I → Type v} [(i : I) → MulOneClass (f i)] : MulOneClass ((i : I) → f i)

Equations

• PiProp.mulOneClass = MulOneClass.mk ⋯ ⋯

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

Equations

• PiProp.addMonoid = let __spread.0 := PiProp.addSemigroup; let __spread.1 := PiProp.addZeroClass; AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) ⋯ ⋯

theorem PiProp.addMonoid.proof_4 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddMonoid (f i)] (n : ℕ) (a : (i : I) → f i) : (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) (n + 1) a = (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) n a + a

theorem PiProp.addMonoid.proof_1 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

theorem PiProp.addMonoid.proof_2 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

theorem PiProp.addMonoid.proof_3 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddMonoid (f i)] (a : (i : I) → f i) : (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) 0 a = 0

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

Equations

• PiProp.monoid = let __spread.0 := PiProp.semigroup; let __spread.1 := PiProp.mulOneClass; Monoid.mk ⋯ ⋯ (fun (n : ℕ) (x : (i : I) → f i) (i : I) => x i ^ n) ⋯ ⋯

theorem PiProp.addCommMonoid.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

instance PiProp.addCommMonoid {I : Prop} {f : I → Type v} [(i : I) → AddCommMonoid (f i)] : AddCommMonoid ((i : I) → f i)

Equations

• PiProp.addCommMonoid = let __spread.0 := PiProp.addMonoid; let __spread.1 := PiProp.addCommSemigroup; AddCommMonoid.mk ⋯

instance PiProp.commMonoid {I : Prop} {f : I → Type v} [(i : I) → CommMonoid (f i)] : CommMonoid ((i : I) → f i)

Equations

• PiProp.commMonoid = let __spread.0 := PiProp.monoid; let __spread.1 := PiProp.commSemigroup; CommMonoid.mk ⋯

theorem PiProp.subNegMonoid.proof_2 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (a : (i : I) → f i), zsmulRec 0 a = zsmulRec 0 a

theorem PiProp.subNegMonoid.proof_1 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubNegMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a - b = a + -b

theorem PiProp.subNegMonoid.proof_4 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (n : ℕ) (a : (i : I) → f i), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem PiProp.subNegMonoid.proof_3 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubNegMonoid (f i)] : ∀ (n : ℕ) (a : (i : I) → f i), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a

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

Equations

• PiProp.subNegMonoid = SubNegMonoid.mk ⋯ zsmulRec ⋯ ⋯ ⋯

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

Equations

• PiProp.divInvMonoid = DivInvMonoid.mk ⋯ zpowRec ⋯ ⋯ ⋯

instance PiProp.hasInvolutiveNeg {I : Prop} {f : I → Type v} [(i : I) → InvolutiveNeg (f i)] : InvolutiveNeg ((i : I) → f i)

Equations

• PiProp.hasInvolutiveNeg = InvolutiveNeg.mk ⋯

theorem PiProp.hasInvolutiveNeg.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → InvolutiveNeg (f i)] (a : (i : I) → f i) : - -a = a

instance PiProp.hasInvolutiveInv {I : Prop} {f : I → Type v} [(i : I) → InvolutiveInv (f i)] : InvolutiveInv ((i : I) → f i)

Equations

• PiProp.hasInvolutiveInv = InvolutiveInv.mk ⋯

theorem PiProp.subtractionMonoid.proof_1 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubtractionMonoid (f i)] (x : (i : I) → f i) : - -x = x

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

Equations

• PiProp.subtractionMonoid = let __spread.0 := PiProp.subNegMonoid; let __spread.1 := PiProp.hasInvolutiveNeg; SubtractionMonoid.mk ⋯ ⋯ ⋯

theorem PiProp.subtractionMonoid.proof_2 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : -(a + b) = -b + -a

theorem PiProp.subtractionMonoid.proof_3 {I : Prop} {f : I → Type u_1} [inst : (i : I) → SubtractionMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (h : a + b = 0) : -a = b

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

Equations

• PiProp.divisionMonoid = let __spread.0 := PiProp.divInvMonoid; let __spread.1 := PiProp.hasInvolutiveInv; DivisionMonoid.mk ⋯ ⋯ ⋯

instance PiProp.subtractionCommMonoid {I : Prop} {f : I → Type v} [(i : I) → SubtractionCommMonoid (f i)] : SubtractionCommMonoid ((i : I) → f i)

Equations

• PiProp.subtractionCommMonoid = let __spread.0 := PiProp.subtractionMonoid; let __spread.1 := PiProp.addCommMonoid; SubtractionCommMonoid.mk ⋯

theorem PiProp.subtractionCommMonoid.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → SubtractionCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

instance PiProp.divisionCommMonoid {I : Prop} {f : I → Type v} [(i : I) → DivisionCommMonoid (f i)] : DivisionCommMonoid ((i : I) → f i)

Equations

• PiProp.divisionCommMonoid = let __spread.0 := PiProp.divisionMonoid; let __spread.1 := PiProp.commMonoid; DivisionCommMonoid.mk ⋯

instance PiProp.addGroup {I : Prop} {f : I → Type v} [(i : I) → AddGroup (f i)] : AddGroup ((i : I) → f i)

Equations

• PiProp.addGroup = let __spread.0 := PiProp.subtractionMonoid; AddGroup.mk ⋯

theorem PiProp.addGroup.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddGroup (f i)] (a : (i : I) → f i) : -a + a = 0

instance PiProp.group {I : Prop} {f : I → Type v} [(i : I) → Group (f i)] : Group ((i : I) → f i)

Equations

• PiProp.group = let __spread.0 := PiProp.divisionMonoid; Group.mk ⋯

instance PiProp.addCommGroup {I : Prop} {f : I → Type v} [(i : I) → AddCommGroup (f i)] : AddCommGroup ((i : I) → f i)

Equations

• PiProp.addCommGroup = let __spread.0 := PiProp.addGroup; let __spread.1 := PiProp.addCommMonoid; AddCommGroup.mk ⋯

theorem PiProp.addCommGroup.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

instance PiProp.commGroup {I : Prop} {f : I → Type v} [(i : I) → CommGroup (f i)] : CommGroup ((i : I) → f i)

Equations

• PiProp.commGroup = let __spread.0 := PiProp.group; let __spread.1 := PiProp.commMonoid; CommGroup.mk ⋯

theorem PiProp.AddLeftCancelSemigroup.proof_1 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddLeftCancelSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) (h : a + b = a + c) : b = c

instance PiProp.AddLeftCancelSemigroup {I : Prop} {f : I → Type v} [inst : (i : I) → AddLeftCancelSemigroup (f i)] : AddLeftCancelSemigroup ((i : I) → f i)

Equations

• PiProp.AddLeftCancelSemigroup = let __spread.0 := PiProp.addSemigroup; AddLeftCancelSemigroup.mk ⋯

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

Equations

• PiProp.leftCancelSemigroup = let __spread.0 := PiProp.semigroup; LeftCancelSemigroup.mk ⋯

theorem PiProp.AddRightCancelSemigroup.proof_1 {I : Prop} {f : I → Type u_1} [inst : (i : I) → AddRightCancelSemigroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) (h : a + b = c + b) : a = c

instance PiProp.AddRightCancelSemigroup {I : Prop} {f : I → Type v} [inst : (i : I) → AddRightCancelSemigroup (f i)] : AddRightCancelSemigroup ((i : I) → f i)

Equations

• PiProp.AddRightCancelSemigroup = let __spread.0 := PiProp.addSemigroup; AddRightCancelSemigroup.mk ⋯

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

Equations

• PiProp.rightCancelSemigroup = let __spread.0 := PiProp.semigroup; RightCancelSemigroup.mk ⋯

theorem PiProp.AddLeftCancelMonoid.proof_5 {I : Prop} {f : I → Type u_1} [(i : I) → AddLeftCancelMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

theorem PiProp.AddLeftCancelMonoid.proof_1 {I : Prop} {f : I → Type u_1} [(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

theorem PiProp.AddLeftCancelMonoid.proof_4 {I : Prop} {f : I → Type u_1} [(i : I) → AddLeftCancelMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

instance PiProp.AddLeftCancelMonoid {I : Prop} {f : I → Type v} [(i : I) → AddLeftCancelMonoid (f i)] : AddLeftCancelMonoid ((i : I) → f i)

Equations

• PiProp.AddLeftCancelMonoid = let __spread.0 := PiProp.addMonoid; let __spread.1 := PiProp.AddLeftCancelSemigroup; AddLeftCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

theorem PiProp.AddLeftCancelMonoid.proof_2 {I : Prop} {f : I → Type u_1} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

theorem PiProp.AddLeftCancelMonoid.proof_3 {I : Prop} {f : I → Type u_1} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

instance PiProp.leftCancelMonoid {I : Prop} {f : I → Type v} [(i : I) → LeftCancelMonoid (f i)] : LeftCancelMonoid ((i : I) → f i)

Equations

• PiProp.leftCancelMonoid = let __spread.0 := PiProp.monoid; let __spread.1 := PiProp.leftCancelSemigroup; LeftCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

theorem PiProp.AddRightCancelMonoid.proof_1 {I : Prop} {f : I → Type u_1} [(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

theorem PiProp.AddRightCancelMonoid.proof_2 {I : Prop} {f : I → Type u_1} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

theorem PiProp.AddRightCancelMonoid.proof_4 {I : Prop} {f : I → Type u_1} [(i : I) → AddRightCancelMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

theorem PiProp.AddRightCancelMonoid.proof_3 {I : Prop} {f : I → Type u_1} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

theorem PiProp.AddRightCancelMonoid.proof_5 {I : Prop} {f : I → Type u_1} [(i : I) → AddRightCancelMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

instance PiProp.AddRightCancelMonoid {I : Prop} {f : I → Type v} [(i : I) → AddRightCancelMonoid (f i)] : AddRightCancelMonoid ((i : I) → f i)

Equations

• PiProp.AddRightCancelMonoid = let __spread.0 := PiProp.addMonoid; let __spread.1 := PiProp.AddRightCancelSemigroup; AddRightCancelMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

instance PiProp.rightCancelMonoid {I : Prop} {f : I → Type v} [(i : I) → RightCancelMonoid (f i)] : RightCancelMonoid ((i : I) → f i)

Equations

• PiProp.rightCancelMonoid = let __spread.0 := PiProp.monoid; let __spread.1 := PiProp.rightCancelSemigroup; RightCancelMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

instance PiProp.AddCancelMonoid {I : Prop} {f : I → Type v} [(i : I) → AddCancelMonoid (f i)] : AddCancelMonoid ((i : I) → f i)

Equations

• PiProp.AddCancelMonoid = let __spread.0 := PiProp.AddLeftCancelMonoid; let __spread.1 := PiProp.AddRightCancelMonoid; AddCancelMonoid.mk ⋯

theorem PiProp.AddCancelMonoid.proof_1 {I : Prop} {f : I → Type 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 + b → a = c

instance PiProp.cancelMonoid {I : Prop} {f : I → Type v} [(i : I) → CancelMonoid (f i)] : CancelMonoid ((i : I) → f i)

Equations

• PiProp.cancelMonoid = let __spread.0 := PiProp.leftCancelMonoid; let __spread.1 := PiProp.rightCancelMonoid; CancelMonoid.mk ⋯

instance PiProp.AddCancelCommMonoid {I : Prop} {f : I → Type v} [(i : I) → AddCancelCommMonoid (f i)] : AddCancelCommMonoid ((i : I) → f i)

Equations

• PiProp.AddCancelCommMonoid = let __spread.0 := PiProp.AddCancelMonoid; let __spread.1 := PiProp.addCommMonoid; AddCancelCommMonoid.mk ⋯

theorem PiProp.AddCancelCommMonoid.proof_1 {I : Prop} {f : I → Type u_1} [(i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

instance PiProp.cancelCommMonoid {I : Prop} {f : I → Type v} [(i : I) → CancelCommMonoid (f i)] : CancelCommMonoid ((i : I) → f i)

Equations

• PiProp.cancelCommMonoid = let __spread.0 := PiProp.cancelMonoid; let __spread.1 := PiProp.commMonoid; CancelCommMonoid.mk ⋯

instance PiProp.mulZeroClass {I : Prop} {f : I → Type v} [(i : I) → MulZeroClass (f i)] : MulZeroClass ((i : I) → f i)

Equations

• PiProp.mulZeroClass = MulZeroClass.mk ⋯ ⋯

instance PiProp.mulZeroOneClass {I : Prop} {f : I → Type v} [(i : I) → MulZeroOneClass (f i)] : MulZeroOneClass ((i : I) → f i)

Equations

• PiProp.mulZeroOneClass = let __spread.0 := PiProp.mulOneClass; let __spread.1 := PiProp.mulZeroClass; MulZeroOneClass.mk ⋯ ⋯

instance PiProp.monoidWithZero {I : Prop} {f : I → Type v} [(i : I) → MonoidWithZero (f i)] : MonoidWithZero ((i : I) → f i)

Equations

• PiProp.monoidWithZero = let __spread.0 := PiProp.monoid; let __spread.1 := PiProp.mulZeroClass; MonoidWithZero.mk ⋯ ⋯

instance PiProp.commMonoidWithZero {I : Prop} {f : I → Type v} [(i : I) → CommMonoidWithZero (f i)] : CommMonoidWithZero ((i : I) → f i)

Equations

• PiProp.commMonoidWithZero = let __spread.0 := PiProp.commMonoid; let __spread.1 := PiProp.mulZeroClass; CommMonoidWithZero.mk ⋯ ⋯