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]

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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.instIsLeftCancelAdd {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.instIsRightCancelAdd {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.instIsCancelAdd {I : Type u} {f : I → Type v₁} [(i : I) → Add (f i)] [∀ (i : I), IsCancelAdd (f i)] : IsCancelAdd ((i : I) → f i)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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

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'