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

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, toIsLeftCancelMul := ⋯ }

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, toIsLeftCancelAdd := ⋯ }

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, toIsRightCancelMul := ⋯ }

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, toIsRightCancelAdd := ⋯ }

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, toIsRightCancelMul := ⋯ }

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, toIsRightCancelAdd := ⋯ }

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 := ⋯, toIsLeftCancelMul := ⋯ }

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 := ⋯, toIsLeftCancelAdd := ⋯ }

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'