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 = { toMul := Pi.instMul, mul_assoc := ⋯ }

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

Equations

• Pi.addSemigroup = { toAdd := Pi.instAdd, add_assoc := ⋯ }

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

Equations

• Pi.commSemigroup = { toSemigroup := Pi.semigroup, mul_comm := ⋯ }

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

Equations

• Pi.addCommSemigroup = { toAddSemigroup := Pi.addSemigroup, add_comm := ⋯ }

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

Equations

• Pi.mulOneClass = { toOne := Pi.instOne, toMul := Pi.instMul, one_mul := ⋯, mul_one := ⋯ }

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

Equations

• Pi.addZeroClass = { toZero := Pi.instZero, toAdd := Pi.instAdd, zero_add := ⋯, add_zero := ⋯ }

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

Equations

• Pi.invOneClass = { toOne := Pi.instOne, toInv := Pi.instInv, inv_one := ⋯ }

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

Equations

• Pi.negZeroClass = { toZero := Pi.instZero, toNeg := Pi.instNeg, neg_zero := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.commMonoid = { toMonoid := Pi.monoid, mul_comm := ⋯ }

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

Equations

• Pi.addCommMonoid = { toAddMonoid := Pi.addMonoid, add_comm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.divInvOneMonoid = { toDivInvMonoid := Pi.divInvMonoid, inv_one := ⋯ }

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

Equations

• Pi.subNegZeroMonoid = { toSubNegMonoid := Pi.subNegMonoid, neg_zero := ⋯ }

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

Equations

• Pi.involutiveInv = { toInv := Pi.instInv, inv_inv := ⋯ }

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

Equations

• Pi.involutiveNeg = { toNeg := Pi.instNeg, neg_neg := ⋯ }

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

Equations

• Pi.divisionMonoid = { toDivInvMonoid := Pi.divInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

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

Equations

• Pi.subtractionMonoid = { toSubNegMonoid := Pi.subNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

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

Equations

• Pi.divisionCommMonoid = { toDivisionMonoid := Pi.divisionMonoid, mul_comm := ⋯ }

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

Equations

• Pi.instSubtractionCommMonoid = { toSubtractionMonoid := Pi.subtractionMonoid, add_comm := ⋯ }

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

Equations

• Pi.group = { toDivInvMonoid := Pi.divInvMonoid, inv_mul_cancel := ⋯ }

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

Equations

• Pi.addGroup = { toSubNegMonoid := Pi.subNegMonoid, neg_add_cancel := ⋯ }

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

Equations

• Pi.commGroup = { toGroup := Pi.group, mul_comm := ⋯ }

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

Equations

• Pi.addCommGroup = { toAddGroup := Pi.addGroup, add_comm := ⋯ }

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 = { toSemigroup := Pi.semigroup, mul_left_cancel := ⋯ }

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

Equations

• Pi.addLeftCancelSemigroup = { toAddSemigroup := Pi.addSemigroup, add_left_cancel := ⋯ }

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

Equations

• Pi.rightCancelSemigroup = { toSemigroup := Pi.semigroup, mul_right_cancel := ⋯ }

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

Equations

• Pi.addRightCancelSemigroup = { toAddSemigroup := Pi.addSemigroup, add_right_cancel := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.cancelMonoid = { toLeftCancelMonoid := Pi.leftCancelMonoid, mul_right_cancel := ⋯ }

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

Equations

• Pi.addCancelMonoid = { toAddLeftCancelMonoid := Pi.addLeftCancelMonoid, add_right_cancel := ⋯ }

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

Equations

• Pi.cancelCommMonoid = { toMonoid := Pi.leftCancelMonoid.toMonoid, mul_comm := ⋯, mul_left_cancel := ⋯ }

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

Equations

• Pi.addCancelCommMonoid = { toAddMonoid := Pi.addLeftCancelMonoid.toAddMonoid, add_comm := ⋯, add_left_cancel := ⋯ }

def Pi.mulSingle {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] (i : ι) (x : M i) (j : ι) : M 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 {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] (i : ι) (x : M i) (j : ι) : M 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 {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] (i : ι) (x : M i) : mulSingle i x i = x

@[simp]

theorem Pi.single_eq_same {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] (i : ι) (x : M i) : single i x i = x

@[simp]

theorem Pi.mulSingle_eq_of_ne {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] {i i' : ι} (h : i' ≠ i) (x : M i) : mulSingle i x i' = 1

@[simp]

theorem Pi.single_eq_of_ne {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] {i i' : ι} (h : i' ≠ i) (x : M i) : single i x i' = 0

@[simp]

theorem Pi.mulSingle_eq_of_ne' {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] {i i' : ι} (h : i ≠ i') (x : M 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' {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] {i i' : ι} (h : i ≠ i') (x : M 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 {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] (i : ι) : mulSingle i 1 = 1

@[simp]

theorem Pi.single_zero {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] (i : ι) : single i 0 = 0

@[simp]

theorem Pi.mulSingle_eq_one_iff {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] {i : ι} {x : M i} : mulSingle i x = 1 ↔ x = 1

@[simp]

theorem Pi.single_eq_zero_iff {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] {i : ι} {x : M i} : single i x = 0 ↔ x = 0

theorem Pi.mulSingle_ne_one_iff {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] {i : ι} {x : M i} : mulSingle i x ≠ 1 ↔ x ≠ 1

theorem Pi.single_ne_zero_iff {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] {i : ι} {x : M i} : single i x ≠ 0 ↔ x ≠ 0

theorem Pi.apply_mulSingle {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} [DecidableEq ι] [(i : ι) → One (M i)] [(i : ι) → One (N i)] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 1 = 1) (i : ι) (x : M i) (j : ι) : f' j (mulSingle i x j) = mulSingle i (f' i x) j

theorem Pi.apply_single {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} [DecidableEq ι] [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 0 = 0) (i : ι) (x : M i) (j : ι) : f' j (single i x j) = single i (f' i x) j

theorem Pi.apply_mulSingle₂ {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 1 1 = 1) (i : ι) (x : M i) (y : N i) (j : ι) : f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

theorem Pi.apply_single₂ {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 0 0 = 0) (i : ι) (x : M i) (y : N i) (j : ι) : f' j (single i x j) (single i y j) = single i (f' i x y) j

theorem Pi.mulSingle_op {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} [DecidableEq ι] [(i : ι) → One (M i)] [(i : ι) → One (N i)] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 1 = 1) (i : ι) (x : M i) : mulSingle i (op i x) = fun (j : ι) => op j (mulSingle i x j)

theorem Pi.single_op {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} [DecidableEq ι] [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 0 = 0) (i : ι) (x : M i) : single i (op i x) = fun (j : ι) => op j (single i x j)

theorem Pi.mulSingle_op₂ {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 1 1 = 1) (i : ι) (x₁ : M i) (x₂ : N i) : mulSingle i (op i x₁ x₂) = fun (j : ι) => op j (mulSingle i x₁ j) (mulSingle i x₂ j)

theorem Pi.single_op₂ {ι : Type u_4} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 0 0 = 0) (i : ι) (x₁ : M i) (x₂ : N i) : single i (op i x₁ x₂) = fun (j : ι) => op j (single i x₁ j) (single i x₂ j)

theorem Pi.mulSingle_injective {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] (i : ι) : Function.Injective (mulSingle i)

theorem Pi.single_injective {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] (i : ι) : Function.Injective (single i)

@[simp]

theorem Pi.mulSingle_inj {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → One (M i)] (i : ι) {x y : M i} : mulSingle i x = mulSingle i y ↔ x = y

@[simp]

theorem Pi.single_inj {ι : Type u_4} {M : ι → Type u_5} [DecidableEq ι] [(i : ι) → Zero (M i)] (i : ι) {x y : M i} : single i x = single i y ↔ x = y

theorem Pi.mulSingle_apply {ι : Type u_4} [DecidableEq ι] {M : Type u_8} [One M] (i : ι) (x : M) (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 {ι : Type u_4} [DecidableEq ι] {M : Type u_8} [Zero M] (i : ι) (x : M) (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 {ι : Type u_4} [DecidableEq ι] {M : Type u_8} [One M] (i : ι) (x : M) (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 {ι : Type u_4} [DecidableEq ι] {M : Type u_8} [Zero M] (i : ι) (x : M) (i' : ι) : single i x i' = single i' x i

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

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