Documentation

Mathlib.Algebra.Group.Pi.Basic

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]

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 ⋯

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

IsLeftCancelMul ((i : I) → f i)

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

IsLeftCancelAdd ((i : I) → f i)

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

IsRightCancelMul ((i : I) → f i)

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

IsRightCancelAdd ((i : I) → f i)

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

IsCancelMul ((i : I) → f i)

instance 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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

single i 0 = 0

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

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) :

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) :

mulSingle i x i' = 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) :

single i x i' = 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 (mulSingle i x j) = 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 (single i x j) = 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 (mulSingle i x j) (mulSingle i y j) = 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 (single i x j) (single i y j) = 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) :

mulSingle i (op i x) = fun (j : I) => op j (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) :

single i (op i x) = fun (j : I) => op j (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) :

mulSingle i (op i x₁ x₂) = fun (j : I) => op j (mulSingle i x₁ j) (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) :

single i (op i x₁ x₂) = fun (j : I) => op j (single i x₁ j) (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 (mulSingle i)

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

Function.Injective (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} :

mulSingle i x = 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} :

single i x = 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 : α → β) :

extend f 1 1 = 1

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

extend f 0 0 = 0

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

extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

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

extend f (g₁ + g₂) (e₁ + e₂) = extend f g₁ e₁ + extend f g₂ e₂

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

extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

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

extend f (-g) (-e) = -extend f g e

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

extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

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

extend f (g₁ - g₂) (e₁ - e₂) = extend f g₁ e₁ - extend f g₂ e₂

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

g ∘ f = const α (g b) ↔ f = const α b

theorem Function.comp_eq_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] [One γ] (f : α → β) {g : β → γ} (hg : 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 : 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 : 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 : Injective g) (hg0 : g 0 = 0) :

g ∘ f ≠ 0 ↔ f ≠ 0

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

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) :

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 (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 (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 (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 (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'