Instances and theorems on pi types

This file provides instances for the typeclass defined in Algebra.Group.Defs. More sophisticated instances are defined in Algebra.Group.Pi.Lemmas files elsewhere.

Porting note

This file relied on the pi_instance tactic, which was not available at the time of porting. The comment --pi_instance is inserted before all fields which were previously derived by pi_instance. See this Zulip discussion: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/not.20porting.20pi_instance]

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

instance Pi.instOne {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : One ((i : I) → f i)

Equations

• Pi.instOne = { one := fun (x : I) => 1 }

instance Pi.instZero {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : Zero ((i : I) → f i)

Equations

• Pi.instZero = { zero := fun (x : I) => 0 }

@[simp]

theorem Pi.one_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → One (f i)] : 1 i = 1

@[simp]

theorem Pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → Zero (f i)] : 0 i = 0

theorem Pi.one_def {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : 1 = fun (x : I) => 1

theorem Pi.zero_def {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : 0 = fun (x : I) => 0

@[simp]

theorem Function.const_one {α : Type u_1} {β : Type u_2} [One β] : Function.const α 1 = 1

@[simp]

theorem Function.const_zero {α : Type u_1} {β : Type u_2} [Zero β] : Function.const α 0 = 0

@[simp]

theorem Pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (x : α → β) : 1 ∘ x = 1

@[simp]

theorem Pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (x : α → β) : 0 ∘ x = 0

@[simp]

theorem Pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] (x : β → γ) : x ∘ 1 = Function.const α (x 1)

@[simp]

theorem Pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] (x : β → γ) : x ∘ 0 = Function.const α (x 0)

instance Pi.instMul {I : Type u} {f : I → Type v₁} [(i : I) → Mul (f i)] : Mul ((i : I) → f i)

Equations

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

instance Pi.instAdd {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] : Add ((i : I) → f i)

Equations

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

@[simp]

theorem Pi.mul_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Mul (f i)] : (x * y) i = x i * y i

@[simp]

theorem Pi.add_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Add (f i)] : (x + y) i = x i + y i

theorem Pi.mul_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Mul (f i)] : x * y = fun (i : I) => x i * y i

theorem Pi.add_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Add (f i)] : x + y = fun (i : I) => x i + y i

@[simp]

theorem Function.const_mul {α : Type u_1} {β : Type u_2} [Mul β] (a b : β) : Function.const α a * Function.const α b = Function.const α (a * b)

@[simp]

theorem Function.const_add {α : Type u_1} {β : Type u_2} [Add β] (a b : β) : Function.const α a + Function.const α b = Function.const α (a + b)

theorem Pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (x y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z

theorem Pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (x y : β → γ) (z : α → β) : (x + y) ∘ z = x ∘ z + y ∘ z

instance Pi.instSMul {I : Type u} {α : Type u_1} {f : I → Type v₁} [(i : I) → SMul α (f i)] : SMul α ((i : I) → f i)

Equations

• Pi.instSMul = { smul := fun (s : α) (x : (i : I) → f i) (i : I) => s • x i }

instance Pi.instVAdd {I : Type u} {α : Type u_1} {f : I → Type v₁} [(i : I) → VAdd α (f i)] : VAdd α ((i : I) → f i)

Equations

• Pi.instVAdd = { vadd := fun (s : α) (x : (i : I) → f i) (i : I) => s +ᵥ x i }

instance Pi.instPow {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] : Pow ((i : I) → f i) β

Equations

• Pi.instPow = { pow := fun (x : (i : I) → f i) (b : β) (i : I) => x i ^ b }

@[simp]

theorem Pi.pow_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) (i : I) : (x ^ b) i = x i ^ b

@[simp]

theorem Pi.vadd_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) (i : I) : (b +ᵥ x) i = b +ᵥ x i

@[simp]

theorem Pi.smul_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) (i : I) : (b • x) i = b • x i

theorem Pi.pow_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) : x ^ b = fun (i : I) => x i ^ b

theorem Pi.smul_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) : b • x = fun (i : I) => b • x i

theorem Pi.vadd_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) : b +ᵥ x = fun (i : I) => b +ᵥ x i

@[simp]

theorem Function.const_pow {I : Type u} {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) : Function.const I a ^ b = Function.const I (a ^ b)

@[simp]

theorem Function.vadd_const {I : Type u} {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : b +ᵥ Function.const I a = Function.const I (b +ᵥ a)

@[simp]

theorem Function.smul_const {I : Type u} {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : b • Function.const I a = Function.const I (b • a)

theorem Pi.pow_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a

theorem Pi.vadd_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] (a : α) (x : β → γ) (y : I → β) : (a +ᵥ x) ∘ y = a +ᵥ x ∘ y

theorem Pi.smul_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α γ] (a : α) (x : β → γ) (y : I → β) : (a • x) ∘ y = a • x ∘ y

instance Pi.instInv {I : Type u} {f : I → Type v₁} [(i : I) → Inv (f i)] : Inv ((i : I) → f i)

Equations

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

instance Pi.instNeg {I : Type u} {f : I → Type v₁} [(i : I) → Neg (f i)] : Neg ((i : I) → f i)

Equations

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

@[simp]

theorem Pi.inv_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Inv (f i)] : x⁻¹ i = (x i)⁻¹

@[simp]

theorem Pi.neg_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Neg (f i)] : (-x) i = -x i

theorem Pi.inv_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Inv (f i)] : x⁻¹ = fun (i : I) => (x i)⁻¹

theorem Pi.neg_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Neg (f i)] : -x = fun (i : I) => -x i

theorem Function.const_inv {α : Type u_1} {β : Type u_2} [Inv β] (a : β) : (Function.const α a)⁻¹ = Function.const α a⁻¹

theorem Function.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) : -Function.const α a = Function.const α (-a)

theorem Pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹

theorem Pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (x : β → γ) (y : α → β) : (-x) ∘ y = -x ∘ y

instance Pi.instDiv {I : Type u} {f : I → Type v₁} [(i : I) → Div (f i)] : Div ((i : I) → f i)

Equations

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

instance Pi.instSub {I : Type u} {f : I → Type v₁} [(i : I) → Sub (f i)] : Sub ((i : I) → f i)

Equations

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

@[simp]

theorem Pi.div_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Div (f i)] : (x / y) i = x i / y i

@[simp]

theorem Pi.sub_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Sub (f i)] : (x - y) i = x i - y i

theorem Pi.div_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Div (f i)] : x / y = fun (i : I) => x i / y i

theorem Pi.sub_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Sub (f i)] : x - y = fun (i : I) => x i - y i

theorem Pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z

theorem Pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (x y : β → γ) (z : α → β) : (x - y) ∘ z = x ∘ z - y ∘ z

@[simp]

theorem Function.const_div {α : Type u_1} {β : Type u_2} [Div β] (a b : β) : Function.const α a / Function.const α b = Function.const α (a / b)

@[simp]

theorem Function.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a b : β) : Function.const α a - Function.const α b = Function.const α (a - b)

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

Equations

• Pi.semigroup = Semigroup.mk ⋯

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

Equations

• Pi.addSemigroup = AddSemigroup.mk ⋯

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

Equations

• Pi.commSemigroup = CommSemigroup.mk ⋯

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

Equations

• Pi.addCommSemigroup = AddCommSemigroup.mk ⋯

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

Equations

• Pi.mulOneClass = MulOneClass.mk ⋯ ⋯

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

Equations

• Pi.addZeroClass = AddZeroClass.mk ⋯ ⋯

instance Pi.invOneClass {I : Type u} {f : I → Type v₁} [(i : I) → InvOneClass (f i)] : InvOneClass ((i : I) → f i)

Equations

• Pi.invOneClass = InvOneClass.mk ⋯

instance Pi.negZeroClass {I : Type u} {f : I → Type v₁} [(i : I) → NegZeroClass (f i)] : NegZeroClass ((i : I) → f i)

Equations

• Pi.negZeroClass = NegZeroClass.mk ⋯

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

Equations

• Pi.monoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (x : (i : I) → f i) (i : I) => x i ^ n) ⋯ ⋯

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

Equations

• Pi.addMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) ⋯ ⋯

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

Equations

• Pi.commMonoid = CommMonoid.mk ⋯

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

Equations

• Pi.addCommMonoid = AddCommMonoid.mk ⋯

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

Equations

• Pi.divInvMonoid = DivInvMonoid.mk ⋯ (fun (z : ℤ) (x : (i : I) → f i) (i : I) => x i ^ z) ⋯ ⋯ ⋯

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

Equations

• Pi.subNegMonoid = SubNegMonoid.mk ⋯ (fun (z : ℤ) (x : (i : I) → f i) (i : I) => z • x i) ⋯ ⋯ ⋯

instance Pi.divInvOneMonoid {I : Type u} {f : I → Type v₁} [(i : I) → DivInvOneMonoid (f i)] : DivInvOneMonoid ((i : I) → f i)

Equations

• Pi.divInvOneMonoid = DivInvOneMonoid.mk ⋯

instance Pi.subNegZeroMonoid {I : Type u} {f : I → Type v₁} [(i : I) → SubNegZeroMonoid (f i)] : SubNegZeroMonoid ((i : I) → f i)

Equations

• Pi.subNegZeroMonoid = SubNegZeroMonoid.mk ⋯

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

Equations

• Pi.involutiveInv = InvolutiveInv.mk ⋯

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

Equations

• Pi.involutiveNeg = InvolutiveNeg.mk ⋯

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

Equations

• Pi.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• Pi.subtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• Pi.divisionCommMonoid = DivisionCommMonoid.mk ⋯

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

Equations

• Pi.instSubtractionCommMonoid = SubtractionCommMonoid.mk ⋯

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

Equations

• Pi.group = Group.mk ⋯

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

Equations

• Pi.addGroup = AddGroup.mk ⋯

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

Equations

• Pi.commGroup = CommGroup.mk ⋯

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

Equations

• Pi.addCommGroup = AddCommGroup.mk ⋯

theorem Pi.instIsLeftCancelMul {I : Type u} {f : I → Type v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsLeftCancelMul (f i)] : IsLeftCancelMul ((i : I) → f i)

theorem Pi.instIsAddLeftCancel {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] [∀ (i : I), IsLeftCancelAdd (f i)] : IsLeftCancelAdd ((i : I) → f i)

theorem Pi.instIsRightCancelMul {I : Type u} {f : I → Type v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsRightCancelMul (f i)] : IsRightCancelMul ((i : I) → f i)

theorem Pi.instIsAddRightCancel {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] [∀ (i : I), IsRightCancelAdd (f i)] : IsRightCancelAdd ((i : I) → f i)

theorem Pi.instIsCancelMul {I : Type u} {f : I → Type v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsCancelMul (f i)] : IsCancelMul ((i : I) → f i)

theorem Pi.instIsAddCancel {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] [∀ (i : I), IsCancelAdd (f i)] : IsCancelAdd ((i : I) → f i)

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

Equations

• Pi.leftCancelSemigroup = LeftCancelSemigroup.mk ⋯

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

Equations

• Pi.addLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

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

Equations

• Pi.rightCancelSemigroup = RightCancelSemigroup.mk ⋯

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

Equations

• Pi.addRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

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

Equations

• Pi.leftCancelMonoid = LeftCancelMonoid.mk ⋯

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

Equations

• Pi.addLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯

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

Equations

• Pi.rightCancelMonoid = RightCancelMonoid.mk ⋯

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

Equations

• Pi.addRightCancelMonoid = AddRightCancelMonoid.mk ⋯

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

Equations

• Pi.cancelMonoid = CancelMonoid.mk ⋯

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

Equations

• Pi.addCancelMonoid = AddCancelMonoid.mk ⋯

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

Equations

• Pi.cancelCommMonoid = CancelCommMonoid.mk ⋯

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

Equations

• Pi.addCancelCommMonoid = AddCancelCommMonoid.mk ⋯

def Pi.mulSingle {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] (i : I) (x : f i) (j : I) : f j

The function supported at i, with value x there, and 1 elsewhere.

Equations

• Pi.mulSingle i x = Function.update 1 i x

def Pi.single {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] (i : I) (x : f i) (j : I) : f j

The function supported at i, with value x there, and 0 elsewhere.

Equations

• Pi.single i x = Function.update 0 i x

@[simp]

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

@[simp]

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

@[simp]

theorem Pi.mulSingle_eq_of_ne {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {i i' : I} (h : i' ≠ i) (x : f i) : Pi.mulSingle i x i' = 1

@[simp]

theorem Pi.single_eq_of_ne {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {i i' : I} (h : i' ≠ i) (x : f i) : Pi.single i x i' = 0

@[simp]

theorem Pi.mulSingle_eq_of_ne' {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {i i' : I} (h : i ≠ i') (x : f i) : Pi.mulSingle i x i' = 1

Abbreviation for mulSingle_eq_of_ne h.symm, for ease of use by simp.

@[simp]

theorem Pi.single_eq_of_ne' {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {i i' : I} (h : i ≠ i') (x : f i) : Pi.single i x i' = 0

Abbreviation for single_eq_of_ne h.symm, for ease of use by simp.

@[simp]

theorem Pi.mulSingle_one {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] (i : I) : Pi.mulSingle i 1 = 1

@[simp]

theorem Pi.single_zero {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] (i : I) : Pi.single i 0 = 0

theorem Pi.mulSingle_apply {I : Type u} {β : Type u_2} [DecidableEq I] [One β] (i : I) (x : β) (i' : I) : Pi.mulSingle i x i' = if i' = i then x else 1

On non-dependent functions, Pi.mulSingle can be expressed as an ite

theorem Pi.single_apply {I : Type u} {β : Type u_2} [DecidableEq I] [Zero β] (i : I) (x : β) (i' : I) : Pi.single i x i' = if i' = i then x else 0

On non-dependent functions, Pi.single can be expressed as an ite

theorem Pi.mulSingle_comm {I : Type u} {β : Type u_2} [DecidableEq I] [One β] (i : I) (x : β) (i' : I) : Pi.mulSingle i x i' = Pi.mulSingle i' x i

On non-dependent functions, Pi.mulSingle is symmetric in the two indices.

theorem Pi.single_comm {I : Type u} {β : Type u_2} [DecidableEq I] [Zero β] (i : I) (x : β) (i' : I) : Pi.single i x i' = Pi.single i' x i

On non-dependent functions, Pi.single is symmetric in the two indices.

theorem Pi.apply_mulSingle {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [DecidableEq I] [(i : I) → One (f i)] [(i : I) → One (g i)] (f' : (i : I) → f i → g i) (hf' : ∀ (i : I), f' i 1 = 1) (i : I) (x : f i) (j : I) : f' j (Pi.mulSingle i x j) = Pi.mulSingle i (f' i x) j

theorem Pi.apply_single {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [DecidableEq I] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] (f' : (i : I) → f i → g i) (hf' : ∀ (i : I), f' i 0 = 0) (i : I) (x : f i) (j : I) : f' j (Pi.single i x j) = Pi.single i (f' i x) j

theorem Pi.apply_mulSingle₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [DecidableEq I] [(i : I) → One (f i)] [(i : I) → One (g i)] [(i : I) → One (h i)] (f' : (i : I) → f i → g i → h i) (hf' : ∀ (i : I), f' i 1 1 = 1) (i : I) (x : f i) (y : g i) (j : I) : f' j (Pi.mulSingle i x j) (Pi.mulSingle i y j) = Pi.mulSingle i (f' i x y) j

theorem Pi.apply_single₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [DecidableEq I] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] [(i : I) → Zero (h i)] (f' : (i : I) → f i → g i → h i) (hf' : ∀ (i : I), f' i 0 0 = 0) (i : I) (x : f i) (y : g i) (j : I) : f' j (Pi.single i x j) (Pi.single i y j) = Pi.single i (f' i x y) j

theorem Pi.mulSingle_op {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {g : I → Type u_4} [(i : I) → One (g i)] (op : (i : I) → f i → g i) (h : ∀ (i : I), op i 1 = 1) (i : I) (x : f i) : Pi.mulSingle i (op i x) = fun (j : I) => op j (Pi.mulSingle i x j)

theorem Pi.single_op {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {g : I → Type u_4} [(i : I) → Zero (g i)] (op : (i : I) → f i → g i) (h : ∀ (i : I), op i 0 = 0) (i : I) (x : f i) : Pi.single i (op i x) = fun (j : I) => op j (Pi.single i x j)

theorem Pi.mulSingle_op₂ {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → One (f i)] {g₁ : I → Type u_4} {g₂ : I → Type u_5} [(i : I) → One (g₁ i)] [(i : I) → One (g₂ i)] (op : (i : I) → g₁ i → g₂ i → f i) (h : ∀ (i : I), op i 1 1 = 1) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) : Pi.mulSingle i (op i x₁ x₂) = fun (j : I) => op j (Pi.mulSingle i x₁ j) (Pi.mulSingle i x₂ j)

theorem Pi.single_op₂ {I : Type u} {f : I → Type v₁} [DecidableEq I] [(i : I) → Zero (f i)] {g₁ : I → Type u_4} {g₂ : I → Type u_5} [(i : I) → Zero (g₁ i)] [(i : I) → Zero (g₂ i)] (op : (i : I) → g₁ i → g₂ i → f i) (h : ∀ (i : I), op i 0 0 = 0) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) : Pi.single i (op i x₁ x₂) = fun (j : I) => op j (Pi.single i x₁ j) (Pi.single i x₂ j)

theorem Pi.mulSingle_injective {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → One (f i)] (i : I) : Function.Injective (Pi.mulSingle i)

theorem Pi.single_injective {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) : Function.Injective (Pi.single i)

@[simp]

theorem Pi.mulSingle_inj {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → One (f i)] (i : I) {x y : f i} : Pi.mulSingle i x = Pi.mulSingle i y ↔ x = y

@[simp]

theorem Pi.single_inj {I : Type u} (f : I → Type v₁) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) {x y : f i} : Pi.single i x = Pi.single i y ↔ x = y

def Pi.prod {I : Type u} {f : I → Type v₁} {g : I → Type v₂} (f' : (i : I) → f i) (g' : (i : I) → g i) (i : I) : f i × g i

The mapping into a product type built from maps into each component.

Equations

• Pi.prod f' g' i = (f' i, g' i)

theorem Pi.prod_fst_snd {α : Type u_1} {β : Type u_2} : Pi.prod Prod.fst Prod.snd = id

theorem Pi.prod_snd_fst {α : Type u_1} {β : Type u_2} : Pi.prod Prod.snd Prod.fst = Prod.swap

theorem Function.extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (f : α → β) : Function.extend f 1 1 = 1

theorem Function.extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (f : α → β) : Function.extend f 0 0 = 0

theorem Function.extend_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) : Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂

theorem Function.extend_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) : Function.extend f (g₁ + g₂) (e₁ + e₂) = Function.extend f g₁ e₁ + Function.extend f g₂ e₂

theorem Function.extend_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) : Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹

theorem Function.extend_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (f : α → β) (g : α → γ) (e : β → γ) : Function.extend f (-g) (-e) = -Function.extend f g e

theorem Function.extend_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) : Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂

theorem Function.extend_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) : Function.extend f (g₁ - g₂) (e₁ - e₂) = Function.extend f g₁ e₁ - Function.extend f g₂ e₂

theorem Function.comp_eq_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (f : α → β) {g : β → γ} (hg : Function.Injective g) : g ∘ f = Function.const α (g b) ↔ f = Function.const α b

theorem Function.comp_eq_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] [One γ] (f : α → β) {g : β → γ} (hg : Function.Injective g) (hg0 : g 1 = 1) : g ∘ f = 1 ↔ f = 1

theorem Function.comp_eq_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] [Zero γ] (f : α → β) {g : β → γ} (hg : Function.Injective g) (hg0 : g 0 = 0) : g ∘ f = 0 ↔ f = 0

theorem Function.comp_ne_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] [One γ] (f : α → β) {g : β → γ} (hg : Function.Injective g) (hg0 : g 1 = 1) : g ∘ f ≠ 1 ↔ f ≠ 1

theorem Function.comp_ne_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] [Zero γ] (f : α → β) {g : β → γ} (hg : Function.Injective g) (hg0 : g 0 = 0) : g ∘ f ≠ 0 ↔ f ≠ 0

def uniqueOfSurjectiveOne (α : Type u_4) {β : Type u_5} [One β] (h : Function.Surjective 1) : Unique β

If the one function is surjective, the codomain is trivial.

Equations

• uniqueOfSurjectiveOne α h = Function.Surjective.uniqueOfSurjectiveConst α 1 h

def uniqueOfSurjectiveZero (α : Type u_4) {β : Type u_5} [Zero β] (h : Function.Surjective 0) : Unique β

If the zero function is surjective, the codomain is trivial.

Equations

• uniqueOfSurjectiveZero α h = Function.Surjective.uniqueOfSurjectiveConst α 0 h

theorem Subsingleton.pi_mulSingle_eq {I : Type u} {α : Type u_4} [DecidableEq I] [Subsingleton I] [One α] (i : I) (x : α) : Pi.mulSingle i x = fun (x_1 : I) => x

theorem Subsingleton.pi_single_eq {I : Type u} {α : Type u_4} [DecidableEq I] [Subsingleton I] [Zero α] (i : I) (x : α) : Pi.single i x = fun (x_1 : I) => x

@[simp]

theorem Sum.elim_one_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] : Sum.elim 1 1 = 1

@[simp]

theorem Sum.elim_zero_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] : Sum.elim 0 0 = 0

@[simp]

theorem Sum.elim_mulSingle_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [One γ] (i : α) (c : γ) : Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (Sum.inl i) c

@[simp]

theorem Sum.elim_single_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [Zero γ] (i : α) (c : γ) : Sum.elim (Pi.single i c) 0 = Pi.single (Sum.inl i) c

@[simp]

theorem Sum.elim_one_mulSingle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) : Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c

@[simp]

theorem Sum.elim_zero_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [Zero γ] (i : β) (c : γ) : Sum.elim 0 (Pi.single i c) = Pi.single (Sum.inr i) c

theorem Sum.elim_inv_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [Inv γ] : Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹

theorem Sum.elim_neg_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [Neg γ] : Sum.elim (-a) (-b) = -Sum.elim a b

theorem Sum.elim_mul_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

theorem Sum.elim_add_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [Add γ] : Sum.elim (a + a') (b + b') = Sum.elim a b + Sum.elim a' b'

theorem Sum.elim_div_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

theorem Sum.elim_sub_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [Sub γ] : Sum.elim (a - a') (b - b') = Sum.elim a b - Sum.elim a' b'