Mathlib.Algebra.Group.Pi.Basic

Pi.semigroup instance

[∀ i, Semigroup (f i)] : Semigroup (∀ i, f i)

Full source

@[to_additive]
instance semigroup [∀ i, Semigroup (f i)] : Semigroup (∀ i, f i) where
  mul_assoc := by intros; ext; exact mul_assoc _ _ _

Pointwise Semigroup Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a semigroup, the product type $\prod_{i \in I} f_i$ is also a semigroup with pointwise multiplication.

Pi.commSemigroup instance

[∀ i, CommSemigroup (f i)] : CommSemigroup (∀ i, f i)

Full source

@[to_additive]
instance commSemigroup [∀ i, CommSemigroup (f i)] : CommSemigroup (∀ i, f i) where
  mul_comm := by intros; ext; exact mul_comm _ _

Pointwise Commutative Semigroup Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative semigroup, the product type $\prod_{i \in I} f_i$ is also a commutative semigroup with pointwise multiplication.

Pi.mulOneClass instance

[∀ i, MulOneClass (f i)] : MulOneClass (∀ i, f i)

Full source

@[to_additive]
instance mulOneClass [∀ i, MulOneClass (f i)] : MulOneClass (∀ i, f i) where
  one_mul := by intros; ext; exact one_mul _
  mul_one := by intros; ext; exact mul_one _

Pointwise `MulOneClass` Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation and a multiplicative identity (i.e., each $f_i$ is a `MulOneClass`), the product type $\prod_{i \in I} f_i$ inherits a `MulOneClass` structure with pointwise multiplication and identity.

Pi.invOneClass instance

[∀ i, InvOneClass (f i)] : InvOneClass (∀ i, f i)

Full source

@[to_additive]
instance invOneClass [∀ i, InvOneClass (f i)] : InvOneClass (∀ i, f i) where
  inv_one := by ext; exact inv_one

Componentwise Inversion and Identity on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with an `InvOneClass` structure (i.e., has an inversion operation and a multiplicative identity), the product type $\prod_{i \in I} f_i$ also inherits an `InvOneClass` structure, where the inversion and identity operations are defined componentwise.

Pi.monoid instance

[∀ i, Monoid (f i)] : Monoid (∀ i, f i)

Full source

@[to_additive]
instance monoid [∀ i, Monoid (f i)] : Monoid (∀ i, f i) where
  __ := semigroup
  __ := mulOneClass
  npow := fun n x i => x i ^ n
  npow_zero := by intros; ext; exact Monoid.npow_zero _
  npow_succ := by intros; ext; exact Monoid.npow_succ _ _

Pointwise Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a monoid, the product type $\prod_{i \in I} f_i$ is also a monoid with pointwise multiplication and identity.

Pi.commMonoid instance

[∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i)

Full source

@[to_additive]
instance commMonoid [∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i) :=
  { monoid, commSemigroup with }

Pointwise Commutative Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative monoid, the product type $\prod_{i \in I} f_i$ is also a commutative monoid with pointwise multiplication and identity.

Pi.divInvMonoid instance

[∀ i, DivInvMonoid (f i)] : DivInvMonoid (∀ i, f i)

Full source

@[to_additive Pi.subNegMonoid]
instance divInvMonoid [∀ i, DivInvMonoid (f i)] : DivInvMonoid (∀ i, f i) where
  zpow := fun z x i => x i ^ z
  div_eq_mul_inv := by intros; ext; exact div_eq_mul_inv _ _
  zpow_zero' := by intros; ext; exact DivInvMonoid.zpow_zero' _
  zpow_succ' := by intros; ext; exact DivInvMonoid.zpow_succ' _ _
  zpow_neg' := by intros; ext; exact DivInvMonoid.zpow_neg' _ _

Pointwise Division Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a division monoid, the product type $\prod_{i \in I} f_i$ is also a division monoid with pointwise division and inversion operations.

Pi.divInvOneMonoid instance

[∀ i, DivInvOneMonoid (f i)] : DivInvOneMonoid (∀ i, f i)

Full source

@[to_additive]
instance divInvOneMonoid [∀ i, DivInvOneMonoid (f i)] : DivInvOneMonoid (∀ i, f i) where
  inv_one := by ext; exact inv_one

Pointwise Division Monoid with Identity Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a division monoid with a multiplicative identity, the product type $\prod_{i \in I} f_i$ is also a division monoid with a multiplicative identity, with pointwise division, inversion, and identity operations.

Pi.involutiveInv instance

[∀ i, InvolutiveInv (f i)] : InvolutiveInv (∀ i, f i)

Full source

@[to_additive]
instance involutiveInv [∀ i, InvolutiveInv (f i)] : InvolutiveInv (∀ i, f i) where
  inv_inv := by intros; ext; exact inv_inv _

Pointwise Involutive Inversion on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ has an involutive inversion operation, the product type $\prod_{i \in I} f_i$ also has an involutive inversion operation defined pointwise.

Pi.divisionMonoid instance

[∀ i, DivisionMonoid (f i)] : DivisionMonoid (∀ i, f i)

Full source

@[to_additive]
instance divisionMonoid [∀ i, DivisionMonoid (f i)] : DivisionMonoid (∀ i, f i) where
  __ := divInvMonoid
  __ := involutiveInv
  mul_inv_rev := by intros; ext; exact mul_inv_rev _ _
  inv_eq_of_mul := by intros _ _ h; ext; exact DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)

Pointwise Division Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a division monoid, the product type $\prod_{i \in I} f_i$ is also a division monoid with pointwise division and inversion operations.

Pi.divisionCommMonoid instance

[∀ i, DivisionCommMonoid (f i)] : DivisionCommMonoid (∀ i, f i)

Full source

@[to_additive instSubtractionCommMonoid]
instance divisionCommMonoid [∀ i, DivisionCommMonoid (f i)] : DivisionCommMonoid (∀ i, f i) :=
  { divisionMonoid, commSemigroup with }

Pointwise Commutative Division Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative division monoid, the product type $\prod_{i \in I} f_i$ is also a commutative division monoid with pointwise division and inversion operations.

Pi.group instance

[∀ i, Group (f i)] : Group (∀ i, f i)

Full source

@[to_additive]
instance group [∀ i, Group (f i)] : Group (∀ i, f i) where
  inv_mul_cancel := by intros; ext; exact inv_mul_cancel _

Pointwise Group Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a group, the product type $\prod_{i \in I} f_i$ is also a group with pointwise multiplication and inversion operations.

Pi.commGroup instance

[∀ i, CommGroup (f i)] : CommGroup (∀ i, f i)

Full source

@[to_additive]
instance commGroup [∀ i, CommGroup (f i)] : CommGroup (∀ i, f i) := { group, commMonoid with }

Pointwise Commutative Group Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a commutative group, the product type $\prod_{i \in I} f_i$ is also a commutative group with pointwise multiplication and inversion operations.

Pi.instIsLeftCancelMul instance

[∀ i, Mul (f i)] [∀ i, IsLeftCancelMul (f i)] : IsLeftCancelMul (∀ i, f i)

Full source

@[to_additive] instance instIsLeftCancelMul [∀ i, Mul (f i)] [∀ i, IsLeftCancelMul (f i)] :
    IsLeftCancelMul (∀ i, f i) where
  mul_left_cancel  _ _ _ h := funext fun _ ↦ mul_left_cancel (congr_fun h _)

Left Cancellation Property for Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation and satisfies the left cancellation property (i.e., $a \cdot b = a \cdot c$ implies $b = c$ for all $a, b, c \in f_i$), the product type $\prod_{i \in I} f_i$ also satisfies the left cancellation property.

Pi.instIsRightCancelMul instance

[∀ i, Mul (f i)] [∀ i, IsRightCancelMul (f i)] : IsRightCancelMul (∀ i, f i)

Full source

@[to_additive] instance instIsRightCancelMul [∀ i, Mul (f i)] [∀ i, IsRightCancelMul (f i)] :
    IsRightCancelMul (∀ i, f i) where
  mul_right_cancel  _ _ _ h := funext fun _ ↦ mul_right_cancel (congr_fun h _)

Right Cancellation Property for Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation and satisfies the right cancellation property (i.e., for all $a, b, c \in f_i$, $a \cdot c = b \cdot c$ implies $a = b$), the product type $\prod_{i \in I} f_i$ also satisfies the right cancellation property.

Pi.instIsCancelMul instance

[∀ i, Mul (f i)] [∀ i, IsCancelMul (f i)] : IsCancelMul (∀ i, f i)

Full source

@[to_additive] instance instIsCancelMul [∀ i, Mul (f i)] [∀ i, IsCancelMul (f i)] :
    IsCancelMul (∀ i, f i) where

Cancellation Property for Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is equipped with a multiplication operation and satisfies both the left and right cancellation properties, the product type $\prod_{i \in I} f_i$ also satisfies both cancellation properties.

Pi.leftCancelSemigroup instance

[∀ i, LeftCancelSemigroup (f i)] : LeftCancelSemigroup (∀ i, f i)

Full source

@[to_additive]
instance leftCancelSemigroup [∀ i, LeftCancelSemigroup (f i)] : LeftCancelSemigroup (∀ i, f i) :=
  { semigroup with mul_left_cancel := fun _ _ _ => mul_left_cancel }

Left Cancellative Semigroup Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a left cancellative semigroup, the product type $\prod_{i \in I} f_i$ is also a left cancellative semigroup with pointwise multiplication. Here, left cancellative means that for all $a, b, c \in f_i$, $a \cdot b = a \cdot c$ implies $b = c$.

Pi.rightCancelSemigroup instance

[∀ i, RightCancelSemigroup (f i)] : RightCancelSemigroup (∀ i, f i)

Full source

@[to_additive]
instance rightCancelSemigroup [∀ i, RightCancelSemigroup (f i)] : RightCancelSemigroup (∀ i, f i) :=
  { semigroup with mul_right_cancel := fun _ _ _ => mul_right_cancel }

Pointwise Right Cancellative Semigroup Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a right cancellative semigroup, the product type $\prod_{i \in I} f_i$ is also a right cancellative semigroup with pointwise multiplication.

Pi.leftCancelMonoid instance

[∀ i, LeftCancelMonoid (f i)] : LeftCancelMonoid (∀ i, f i)

Full source

@[to_additive]
instance leftCancelMonoid [∀ i, LeftCancelMonoid (f i)] : LeftCancelMonoid (∀ i, f i) :=
  { leftCancelSemigroup, monoid with }

Pointwise Left Cancellative Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a left cancellative monoid, the product type $\prod_{i \in I} f_i$ is also a left cancellative monoid with pointwise multiplication and identity. Here, left cancellative means that for all $a, b, c \in f_i$, $a \cdot b = a \cdot c$ implies $b = c$.

Pi.rightCancelMonoid instance

[∀ i, RightCancelMonoid (f i)] : RightCancelMonoid (∀ i, f i)

Full source

@[to_additive]
instance rightCancelMonoid [∀ i, RightCancelMonoid (f i)] : RightCancelMonoid (∀ i, f i) :=
  { rightCancelSemigroup, monoid with }

Pointwise Right Cancellative Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a right cancellative monoid, the product type $\prod_{i \in I} f_i$ is also a right cancellative monoid with pointwise multiplication and identity.

Pi.cancelMonoid instance

[∀ i, CancelMonoid (f i)] : CancelMonoid (∀ i, f i)

Full source

@[to_additive]
instance cancelMonoid [∀ i, CancelMonoid (f i)] : CancelMonoid (∀ i, f i) :=
  { leftCancelMonoid, rightCancelMonoid with }

Pointwise Cancellative Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a cancellative monoid, the product type $\prod_{i \in I} f_i$ is also a cancellative monoid with pointwise multiplication and identity. Here, cancellative means that for all $a, b, c \in f_i$, $a \cdot b = a \cdot c$ implies $b = c$ and $b \cdot a = c \cdot a$ implies $b = c$.

Pi.cancelCommMonoid instance

[∀ i, CancelCommMonoid (f i)] : CancelCommMonoid (∀ i, f i)

Full source

@[to_additive]
instance cancelCommMonoid [∀ i, CancelCommMonoid (f i)] : CancelCommMonoid (∀ i, f i) :=
  { leftCancelMonoid, commMonoid with }

Pointwise Cancellative Commutative Monoid Structure on Product Types

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is a cancellative commutative monoid, the product type $\prod_{i \in I} f_i$ is also a cancellative commutative monoid with pointwise multiplication and identity. Here, cancellative means that for all $a, b, c \in f_i$, $a \cdot b = a \cdot c$ implies $b = c$ and $b \cdot a = c \cdot a$ implies $b = c$.

Pi.mulSingle definition

(i : I) (x : f i) : ∀ (j : I), f j

Full source

/-- The function supported at `i`, with value `x` there, and `1` elsewhere. -/
@[to_additive "The function supported at `i`, with value `x` there, and `0` elsewhere."]
def mulSingle (i : I) (x : f i) : ∀ (j : I), f j :=
  Function.update 1 i x

Multiplicative single function on a product type

Informal description

The function `Pi.mulSingle` takes an index `i : I` and a value `x : f i`, and returns a function that is equal to the multiplicative identity `1` everywhere except at `i`, where it takes the value `x`. Formally, for any `j : I`, the function is defined as: \[ \text{mulSingle } i \, x \, j = \begin{cases} x & \text{if } j = i, \\ 1 & \text{otherwise.} \end{cases} \]

Pi.mulSingle_eq_same theorem

(i : I) (x : f i) : mulSingle i x i = x

Full source

@[to_additive (attr := simp)]
theorem mulSingle_eq_same (i : I) (x : f i) : mulSingle i x i = x :=
  Function.update_self i x _

Multiplicative Single Function Identity at Same Index

Informal description

For any index $i$ in a type $I$ and any element $x$ of type $f i$, the multiplicative single function $\text{mulSingle } i \, x$ evaluated at $i$ equals $x$, i.e., $\text{mulSingle } i \, x \, i = x$.

Pi.mulSingle_eq_of_ne theorem

{i i' : I} (h : i' ≠ i) (x : f i) : mulSingle i x i' = 1

Full source

@[to_additive (attr := simp)]
theorem mulSingle_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : mulSingle i x i' = 1 :=
  Function.update_of_ne h x _

Multiplicative Single Function Identity at Distinct Indices

Informal description

For any distinct indices $i$ and $i'$ in a type $I$ (i.e., $i' \neq i$) and any element $x$ of type $f i$, the multiplicative single function $\text{mulSingle } i \, x$ evaluated at $i'$ equals the multiplicative identity $1$, i.e., $\text{mulSingle } i \, x \, i' = 1$.

Pi.mulSingle_eq_of_ne' theorem

{i i' : I} (h : i ≠ i') (x : f i) : mulSingle i x i' = 1

Full source

/-- Abbreviation for `mulSingle_eq_of_ne h.symm`, for ease of use by `simp`. -/
@[to_additive (attr := simp)
  "Abbreviation for `single_eq_of_ne h.symm`, for ease of use by `simp`."]
theorem mulSingle_eq_of_ne' {i i' : I} (h : i ≠ i') (x : f i) : mulSingle i x i' = 1 :=
  mulSingle_eq_of_ne h.symm x

Multiplicative Single Function Identity at Distinct Indices (Symmetric Version)

Informal description

For any distinct indices $i$ and $i'$ in a type $I$ (i.e., $i \neq i'$) and any element $x$ of type $f i$, the multiplicative single function $\text{mulSingle } i \, x$ evaluated at $i'$ equals the multiplicative identity $1$, i.e., $\text{mulSingle } i \, x \, i' = 1$.

Pi.mulSingle_one theorem

(i : I) : mulSingle i (1 : f i) = 1

Full source

@[to_additive (attr := simp)]
theorem mulSingle_one (i : I) : mulSingle i (1 : f i) = 1 :=
  Function.update_eq_self _ _

Multiplicative Single Function with Identity is Constant One

Informal description

For any index $i$ in a type $I$, the multiplicative single function $\text{mulSingle}$ evaluated at $i$ with the multiplicative identity $1$ is equal to the constant function $1$, i.e., $\text{mulSingle } i \, 1 = 1$.

Pi.mulSingle_eq_one_iff theorem

{i : I} {x : f i} : mulSingle i x = 1 ↔ x = 1

Full source

@[to_additive (attr := simp)]
theorem mulSingle_eq_one_iff {i : I} {x : f i} : mulSinglemulSingle i x = 1 ↔ x = 1 := by
  refine ⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩
  rw [← mulSingle_eq_same i x, h, one_apply]

Characterization of Multiplicative Single Function Being One: $\text{mulSingle}_i(x) = 1 \leftrightarrow x = 1$

Informal description

For any index $i$ in a type $I$ and any element $x$ of type $f i$, the multiplicative single function $\text{mulSingle}_i(x)$ is equal to the constant function $1$ if and only if $x$ is equal to the multiplicative identity $1$, i.e., \[ \text{mulSingle}_i(x) = 1 \leftrightarrow x = 1. \]

Pi.mulSingle_ne_one_iff theorem

{i : I} {x : f i} : mulSingle i x ≠ 1 ↔ x ≠ 1

Full source

@[to_additive]
theorem mulSingle_ne_one_iff {i : I} {x : f i} : mulSinglemulSingle i x ≠ 1mulSingle i x ≠ 1 ↔ x ≠ 1 :=
  mulSingle_eq_one_iff.ne

Characterization of Multiplicative Single Function Not Being One: $\text{mulSingle}_i(x) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any index $i$ in a type $I$ and any element $x$ of type $f i$, the multiplicative single function $\text{mulSingle}_i(x)$ is not equal to the constant function $1$ if and only if $x$ is not equal to the multiplicative identity $1$, i.e., \[ \text{mulSingle}_i(x) \neq 1 \leftrightarrow x \neq 1. \]

Pi.mulSingle_apply theorem

[One β] (i : I) (x : β) (i' : I) : (mulSingle i x : I → β) i' = if i' = i then x else 1

Full source

/-- On non-dependent functions, `Pi.mulSingle` can be expressed as an `ite` -/
@[to_additive "On non-dependent functions, `Pi.single` can be expressed as an `ite`"]
theorem mulSingle_apply [One β] (i : I) (x : β) (i' : I) :
    (mulSingle i x : I → β) i' = if i' = i then x else 1 :=
  Function.update_apply (1 : I → β) i x i'

Evaluation of Multiplicative Single Function

Informal description

For any type $I$ and any type $\beta$ with a multiplicative identity $1$, the function $\text{mulSingle}_i(x) : I \to \beta$ (defined for $i \in I$ and $x \in \beta$) satisfies: \[ \text{mulSingle}_i(x)(i') = \begin{cases} x & \text{if } i' = i, \\ 1 & \text{otherwise.} \end{cases} \]

Pi.mulSingle_comm theorem

[One β] (i : I) (x : β) (i' : I) : (mulSingle i x : I → β) i' = (mulSingle i' x : I → β) i

Full source

/-- On non-dependent functions, `Pi.mulSingle` is symmetric in the two indices. -/
@[to_additive "On non-dependent functions, `Pi.single` is symmetric in the two indices."]
theorem mulSingle_comm [One β] (i : I) (x : β) (i' : I) :
    (mulSingle i x : I → β) i' = (mulSingle i' x : I → β) i := by
  simp [mulSingle_apply, eq_comm]

Symmetry of Multiplicative Single Functions: $\text{mulSingle}_i(x)(i') = \text{mulSingle}_{i'}(x)(i)$

Informal description

For any type $I$ and any type $\beta$ with a multiplicative identity $1$, the multiplicative single functions satisfy the symmetry property: \[ \text{mulSingle}_i(x)(i') = \text{mulSingle}_{i'}(x)(i) \] for all $i, i' \in I$ and $x \in \beta$.

Pi.apply_mulSingle theorem

 (f' : ∀ i, f i → g i) (hf' : ∀ i, f' i 1 = 1) (i : I) (x : f i) (j : I) :
  f' j (mulSingle i x j) = mulSingle i (f' i x) j

Full source

@[to_additive]
theorem apply_mulSingle (f' : ∀ i, f i → g i) (hf' : ∀ i, f' i 1 = 1) (i : I) (x : f i) (j : I) :
    f' j (mulSingle i x j) = mulSingle i (f' i x) j := by
  simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j

Compatibility of Function Application with Multiplicative Single Functions

Informal description

Let $I$ be a type, and for each $i \in I$, let $f_i$ and $g_i$ be types equipped with multiplicative identities $1$. Given a family of functions $f' : \prod_{i \in I} (f_i \to g_i)$ such that each $f'_i$ maps the identity $1$ to the identity in $g_i$, then for any $i \in I$, element $x \in f_i$, and any $j \in I$, we have: \[ f'_j \big(\text{mulSingle}_i(x)(j)\big) = \text{mulSingle}_i(f'_i(x))(j), \] where $\text{mulSingle}_i(z)$ denotes the function that is $z$ at $i$ and $1$ elsewhere.

Pi.apply_mulSingle₂ theorem

 (f' : ∀ i, f i → g i → h i) (hf' : ∀ 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

Full source

@[to_additive apply_single₂]
theorem apply_mulSingle₂ (f' : ∀ i, f i → g i → h i) (hf' : ∀ 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 := by
  by_cases h : j = i
  · subst h
    simp only [mulSingle_eq_same]
  · simp only [mulSingle_eq_of_ne h, hf']

Compatibility of Binary Operations with Multiplicative Single Functions

Informal description

Let $I$ be a type, and for each $i \in I$, let $f_i$, $g_i$, and $h_i$ be types equipped with multiplicative identities $1$. Given a family of binary operations $f' : \prod_{i \in I} (f_i \to g_i \to h_i)$ such that each $f'_i$ maps the pair of identities $(1, 1)$ to the identity in $h_i$, then for any $i \in I$, elements $x \in f_i$ and $y \in g_i$, and any $j \in I$, we have: \[ f'_j \big(\text{mulSingle}_i(x)(j), \text{mulSingle}_i(y)(j)\big) = \text{mulSingle}_i(f'_i(x, y))(j), \] where $\text{mulSingle}_i(z)$ denotes the function that is $z$ at $i$ and $1$ elsewhere.

Pi.mulSingle_op theorem

 {g : I → Type*} [∀ i, One (g i)] (op : ∀ i, f i → g i) (h : ∀ i, op i 1 = 1) (i : I) (x : f i) :
  mulSingle i (op i x) = fun j => op j (mulSingle i x j)

Full source

@[to_additive]
theorem mulSingle_op {g : I → Type*} [∀ i, One (g i)] (op : ∀ i, f i → g i)
    (h : ∀ i, op i 1 = 1) (i : I) (x : f i) :
    mulSingle i (op i x) = fun j => op j (mulSingle i x j) :=
  Eq.symm <| funext <| apply_mulSingle op h i x

Compatibility of Unary Operations with Multiplicative Single Functions

Informal description

Let $I$ be a type, and for each $i \in I$, let $f_i$ and $g_i$ be types equipped with multiplicative identities $1$. Given a family of unary operations $\text{op} : \prod_{i \in I} (f_i \to g_i)$ such that each $\text{op}_i$ maps the identity $1$ to the identity in $g_i$, then for any index $i \in I$ and element $x \in f_i$, the following equality holds: \[ \text{mulSingle}_i (\text{op}_i x) = \lambda j, \text{op}_j (\text{mulSingle}_i x \, j), \] where $\text{mulSingle}_i(z)$ denotes the function that is $z$ at $i$ and $1$ elsewhere.

Pi.mulSingle_op₂ theorem

 {g₁ g₂ : I → Type*} [∀ i, One (g₁ i)] [∀ i, One (g₂ i)] (op : ∀ i, g₁ i → g₂ i → f i) (h : ∀ i, op i 1 1 = 1) (i : I)
  (x₁ : g₁ i) (x₂ : g₂ i) : mulSingle i (op i x₁ x₂) = fun j => op j (mulSingle i x₁ j) (mulSingle i x₂ j)

Full source

@[to_additive]
theorem mulSingle_op₂ {g₁ g₂ : I → Type*} [∀ i, One (g₁ i)] [∀ i, One (g₂ i)]
    (op : ∀ i, g₁ i → g₂ i → f i) (h : ∀ i, op i 1 1 = 1) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
    mulSingle i (op i x₁ x₂) = fun j => op j (mulSingle i x₁ j) (mulSingle i x₂ j) :=
  Eq.symm <| funext <| apply_mulSingle₂ op h i x₁ x₂

Compatibility of Binary Operations with Multiplicative Single Functions in Product Types

Informal description

Let $I$ be a type, and for each $i \in I$, let $g_1(i)$, $g_2(i)$, and $f(i)$ be types equipped with multiplicative identities $1$. Given a family of binary operations $\text{op} : \prod_{i \in I} (g_1(i) \to g_2(i) \to f(i))$ such that each $\text{op}_i$ maps the pair of identities $(1, 1)$ to the identity in $f(i)$, then for any index $i \in I$ and elements $x_1 \in g_1(i)$, $x_2 \in g_2(i)$, the following equality holds: \[ \text{mulSingle}_i (\text{op}_i x_1 x_2) = \lambda j, \text{op}_j (\text{mulSingle}_i x_1 j) (\text{mulSingle}_i x_2 j), \] where $\text{mulSingle}_i(z)$ denotes the function that is $z$ at $i$ and $1$ elsewhere.

Pi.mulSingle_injective theorem

(i : I) : Function.Injective (mulSingle i : f i → ∀ i, f i)

Full source

@[to_additive]
theorem mulSingle_injective (i : I) : Function.Injective (mulSingle i : f i → ∀ i, f i) :=
  Function.update_injective _ i

Injectivity of Multiplicative Single Function at Each Index

Informal description

For any index $i \in I$, the function $\text{mulSingle}_i : f(i) \to \prod_{j \in I} f(j)$ is injective. That is, for any $x, y \in f(i)$, if $\text{mulSingle}_i(x) = \text{mulSingle}_i(y)$, then $x = y$.

Pi.mulSingle_inj theorem

(i : I) {x y : f i} : mulSingle i x = mulSingle i y ↔ x = y

Full source

@[to_additive (attr := simp)]
theorem mulSingle_inj (i : I) {x y : f i} : mulSinglemulSingle i x = mulSingle i y ↔ x = y :=
  (Pi.mulSingle_injective _ _).eq_iff

Injectivity Criterion for Multiplicative Single Functions: $\text{mulSingle}_i(x) = \text{mulSingle}_i(y) \leftrightarrow x = y$

Informal description

For any index $i \in I$ and elements $x, y \in f(i)$, the multiplicative single functions $\text{mulSingle}_i(x)$ and $\text{mulSingle}_i(y)$ are equal if and only if $x = y$.

Pi.prod definition

(f' : ∀ i, f i) (g' : ∀ i, g i) (i : I) : f i × g i

Full source

/-- The mapping into a product type built from maps into each component. -/
@[simp]
protected def prod (f' : ∀ i, f i) (g' : ∀ i, g i) (i : I) : f i × g i :=
  (f' i, g' i)

Component-wise product of functions

Informal description

For each index $i$ in the type $I$, the function maps a pair of functions $(f', g')$ to the product $(f'(i), g'(i))$ in the product type $f(i) \times g(i)$.

Pi.prod_fst_snd theorem

: Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id

Full source

theorem prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id :=
  rfl

Product of Projections is Identity

Informal description

The component-wise product of the projection functions $\operatorname{fst} : \alpha \times \beta \to \alpha$ and $\operatorname{snd} : \alpha \times \beta \to \beta$ equals the identity function on $\alpha \times \beta$, i.e., $\operatorname{prod}(\operatorname{fst}, \operatorname{snd}) = \operatorname{id}$.

Pi.prod_snd_fst theorem

: Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = Prod.swap

Full source

theorem prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = Prod.swap :=
  rfl

Component-wise Product of Projections Equals Swap Function

Informal description

For any types $\alpha$ and $\beta$, the component-wise product of the projection functions $\operatorname{snd} : \alpha \times \beta \to \beta$ and $\operatorname{fst} : \alpha \times \beta \to \alpha$ equals the swap function $\operatorname{swap} : \alpha \times \beta \to \beta \times \alpha$. That is, $\Pi.\operatorname{prod}(\operatorname{snd}, \operatorname{fst}) = \operatorname{swap}$.

Function.extend_one theorem

[One γ] (f : α → β) : Function.extend f (1 : α → γ) (1 : β → γ) = 1

Full source

@[to_additive]
theorem extend_one [One γ] (f : α → β) : Function.extend f (1 : α → γ) (1 : β → γ) = 1 :=
  funext fun _ => by apply ite_self

Extension of Constant One Function is One

Informal description

Let $\gamma$ be a type with a multiplicative identity $1$, and let $f : \alpha \to \beta$ be a function. Then the extension of $f$ with the constant function $1 : \alpha \to \gamma$ and the constant function $1 : \beta \to \gamma$ is equal to the constant function $1 : \beta \to \gamma$, i.e., \[ \text{extend}\,f\,(1 : \alpha \to \gamma)\,(1 : \beta \to \gamma) = 1. \]

Function.extend_mul theorem

 [Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
  Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂

Full source

@[to_additive]
theorem extend_mul [Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
    Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂ := by
  classical
  funext x
  simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]

Extension Preserves Pointwise Multiplication

Informal description

Let $\gamma$ be a type equipped with a multiplication operation. For any functions $f : \alpha \to \beta$, $g_1, g_2 : \alpha \to \gamma$, and $e_1, e_2 : \beta \to \gamma$, the extension of $f$ applied to the pointwise product $g_1 * g_2$ with default values $e_1 * e_2$ is equal to the product of the extensions of $f$ applied to $g_1$ and $g_2$ with default values $e_1$ and $e_2$ respectively. That is: \[ \text{extend}\,f\,(g_1 * g_2)\,(e_1 * e_2) = \text{extend}\,f\,g_1\,e_1 * \text{extend}\,f\,g_2\,e_2 \]

Function.extend_inv theorem

 [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) : Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹

Full source

@[to_additive]
theorem extend_inv [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) :
    Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹ := by
  classical
  funext x
  simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]

Extension Preserves Pointwise Inversion

Informal description

Let $\gamma$ be a type equipped with an inversion operation. For any functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, and $e : \beta \to \gamma$, the extension of $f$ applied to the pointwise inverse $g^{-1}$ with default values $e^{-1}$ is equal to the inverse of the extension of $f$ applied to $g$ with default values $e$. That is: \[ \text{extend}\,f\,g^{-1}\,e^{-1} = (\text{extend}\,f\,g\,e)^{-1} \]

Function.extend_div theorem

 [Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
  Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂

Full source

@[to_additive]
theorem extend_div [Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
    Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂ := by
  classical
  funext x
  simp [Function.extend_def, apply_dite₂]

Extension Preserves Pointwise Division

Informal description

Let $\gamma$ be a type equipped with a division operation. For any functions $f : \alpha \to \beta$, $g_1, g_2 : \alpha \to \gamma$, and $e_1, e_2 : \beta \to \gamma$, the extension of $f$ applied to the pointwise division $g_1 / g_2$ with default values $e_1 / e_2$ is equal to the division of the extensions of $f$ applied to $g_1$ and $g_2$ with default values $e_1$ and $e_2$ respectively. That is: \[ \text{extend}\,f\,(g_1 / g_2)\,(e_1 / e_2) = \text{extend}\,f\,g_1\,e_1 / \text{extend}\,f\,g_2\,e_2 \]

Function.comp_eq_const_iff theorem

 (b : β) (f : α → β) {g : β → γ} (hg : Injective g) : g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b

Full source

lemma comp_eq_const_iff (b : β) (f : α → β) {g : β → γ} (hg : Injective g) :
    g ∘ fg ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=
  hg.comp_left.eq_iff' rfl

Composition Equals Constant Function iff Function is Constant (Injective Case)

Informal description

Let $b \in \beta$, $f : \alpha \to \beta$, and $g : \beta \to \gamma$ be an injective function. Then the composition $g \circ f$ is equal to the constant function with value $g(b)$ if and only if $f$ is equal to the constant function with value $b$.

Function.comp_eq_one_iff theorem

[One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) : g ∘ f = 1 ↔ f = 1

Full source

@[to_additive]
lemma comp_eq_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :
    g ∘ fg ∘ f = 1 ↔ f = 1 := by
  simpa [hg0, const_one] using comp_eq_const_iff 1 f hg

Composition Equals Identity iff Function is Constant Identity (Injective Case)

Informal description

Let $\beta$ and $\gamma$ be types with multiplicative identities $1_\beta$ and $1_\gamma$ respectively. For any function $f : \alpha \to \beta$ and an injective function $g : \beta \to \gamma$ such that $g(1_\beta) = 1_\gamma$, the composition $g \circ f$ equals the constant function $1_\gamma$ if and only if $f$ equals the constant function $1_\beta$.

Function.comp_ne_one_iff theorem

[One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) : g ∘ f ≠ 1 ↔ f ≠ 1

Full source

@[to_additive]
lemma comp_ne_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :
    g ∘ fg ∘ f ≠ 1g ∘ f ≠ 1 ↔ f ≠ 1 :=
  (comp_eq_one_iff f hg hg0).ne

Composition Not Equal to Identity iff Function Not Constant Identity (Injective Case)

Informal description

Let $\beta$ and $\gamma$ be types with multiplicative identities $1_\beta$ and $1_\gamma$ respectively. For any function $f : \alpha \to \beta$ and an injective function $g : \beta \to \gamma$ such that $g(1_\beta) = 1_\gamma$, the composition $g \circ f$ is not equal to the constant function $1_\gamma$ if and only if $f$ is not equal to the constant function $1_\beta$.

uniqueOfSurjectiveOne definition

(α : Type*) {β : Type*} [One β] (h : Function.Surjective (1 : α → β)) : Unique β

Full source

/-- If the one function is surjective, the codomain is trivial. -/
@[to_additive "If the zero function is surjective, the codomain is trivial."]
def uniqueOfSurjectiveOne (α : Type*) {β : Type*} [One β] (h : Function.Surjective (1 : α → β)) :
    Unique β :=
  h.uniqueOfSurjectiveConst α (1 : β)

Uniqueness of codomain of a surjective constant one function

Informal description

Given a type $\beta$ with a multiplicative identity element $1$, if the constant function $1 : \alpha \to \beta$ is surjective, then $\beta$ has exactly one element (namely $1$).

Subsingleton.pi_mulSingle_eq theorem

{α : Type*} [DecidableEq I] [Subsingleton I] [One α] (i : I) (x : α) : Pi.mulSingle i x = fun _ => x

Full source

@[to_additive]
theorem Subsingleton.pi_mulSingle_eq {α : Type*} [DecidableEq I] [Subsingleton I] [One α]
    (i : I) (x : α) : Pi.mulSingle i x = fun _ => x :=
  funext fun j => by rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

Multiplicative Single Function Equals Constant Function on Subsingleton Index Type

Informal description

Let $I$ be a type with decidable equality and at most one element (i.e., a subsingleton), and let $\alpha$ be a type with a multiplicative identity $1$. For any index $i \in I$ and any element $x \in \alpha$, the multiplicative single function $\mathrm{mulSingle}_i\, x$ is equal to the constant function that maps every input to $x$. In other words: \[ \mathrm{mulSingle}_i\, x = (\lambda \_, x) \]

Sum.elim_one_one theorem

[One γ] : Sum.elim (1 : α → γ) (1 : β → γ) = 1

Full source

@[to_additive (attr := simp)]
theorem elim_one_one [One γ] : Sum.elim (1 : α → γ) (1 : β → γ) = 1 :=
  Sum.elim_const_const 1

Sum Elimination of Constant One Functions Yields One

Informal description

For any type $\gamma$ with a multiplicative identity element $1$, the function `Sum.elim` applied to the constant functions $1 : \alpha \to \gamma$ and $1 : \beta \to \gamma$ yields the constant function $1 : \alpha \oplus \beta \to \gamma$.

Sum.elim_mulSingle_one theorem

 [DecidableEq α] [DecidableEq β] [One γ] (i : α) (c : γ) :
  Sum.elim (Pi.mulSingle i c) (1 : β → γ) = Pi.mulSingle (Sum.inl i) c

Full source

@[to_additive (attr := simp)]
theorem elim_mulSingle_one [DecidableEq α] [DecidableEq β] [One γ] (i : α) (c : γ) :
    Sum.elim (Pi.mulSingle i c) (1 : β → γ) = Pi.mulSingle (Sum.inl i) c := by
  simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]

Sum Elimination of Multiplicative Single and One Yields Multiplicative Single on Left Injection

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $\gamma$ be a type with a multiplicative identity $1$. For any index $i \in \alpha$ and any element $c \in \gamma$, the sum elimination of the multiplicative single function at $i$ with value $c$ (on $\alpha \to \gamma$) and the constant one function (on $\beta \to \gamma$) equals the multiplicative single function at $\mathrm{Sum.inl}(i)$ with value $c$ (on $\alpha \oplus \beta \to \gamma$). In other words: \[ \mathrm{Sum.elim}\ (\mathrm{mulSingle}_i\ c)\ \mathbf{1} = \mathrm{mulSingle}_{\mathrm{inl}(i)}\ c \] where $\mathbf{1}$ denotes the constant one function.

Sum.elim_one_mulSingle theorem

 [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) :
  Sum.elim (1 : α → γ) (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c

Full source

@[to_additive (attr := simp)]
theorem elim_one_mulSingle [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) :
    Sum.elim (1 : α → γ) (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c := by
  simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]

Sum Elimination of One and Multiplicative Single Yields Multiplicative Single on Right Injection

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $\gamma$ be a type with a multiplicative identity $1$. For any index $i \in \beta$ and any element $c \in \gamma$, the sum elimination of the constant one function (on $\alpha \to \gamma$) and the multiplicative single function at $i$ with value $c$ (on $\beta \to \gamma$) equals the multiplicative single function at $\mathrm{Sum.inr}(i)$ with value $c$ (on $\alpha \oplus \beta \to \gamma$). In other words: \[ \mathrm{Sum.elim}\ \mathbf{1}\ (\mathrm{mulSingle}_i\ c) = \mathrm{mulSingle}_{\mathrm{inr}(i)}\ c \] where $\mathbf{1}$ denotes the constant one function.

Sum.elim_inv_inv theorem

[Inv γ] : Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹

Full source

@[to_additive]
theorem elim_inv_inv [Inv γ] : Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹ :=
  (Sum.comp_elim Inv.inv a b).symm

Inversion Commutes with Sum Elimination

Informal description

For any type $\gamma$ with an inversion operation and any functions $a : \alpha \to \gamma$ and $b : \beta \to \gamma$, the pointwise inversion of the combined function $\mathrm{Sum.elim}\ a\ b$ equals the combination of the pointwise inverses of $a$ and $b$. That is, $$ \mathrm{Sum.elim}\ (a^{-1})\ (b^{-1}) = (\mathrm{Sum.elim}\ a\ b)^{-1}. $$

Sum.elim_mul_mul theorem

[Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Full source

@[to_additive]
theorem elim_mul_mul [Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b' := by
  ext x
  cases x <;> rfl

Multiplication Commutes with Sum Elimination

Informal description

For any type $\gamma$ with a multiplication operation and any functions $a, a' : \alpha \to \gamma$ and $b, b' : \beta \to \gamma$, the pointwise product of the combined functions $\mathrm{Sum.elim}\ a\ b$ and $\mathrm{Sum.elim}\ a'\ b'$ equals the combination of the pointwise products of $a$ with $a'$ and $b$ with $b'$. That is, $$ \mathrm{Sum.elim}\ (a \cdot a')\ (b \cdot b') = (\mathrm{Sum.elim}\ a\ b) \cdot (\mathrm{Sum.elim}\ a'\ b'). $$

Sum.elim_div_div theorem

[Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Full source

@[to_additive]
theorem elim_div_div [Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b' := by
  ext x
  cases x <;> rfl

Division Commutes with Sum Elimination

Informal description

For any type $\gamma$ with a division operation and any functions $a, a' : \alpha \to \gamma$ and $b, b' : \beta \to \gamma$, the pointwise division of the combined functions $\mathrm{Sum.elim}\ a\ b$ and $\mathrm{Sum.elim}\ a'\ b'$ equals the combination of the pointwise divisions of $a$ and $a'$ and of $b$ and $b'$. That is, $$ \mathrm{Sum.elim}\ (a / a')\ (b / b') = (\mathrm{Sum.elim}\ a\ b) / (\mathrm{Sum.elim}\ a'\ b'). $$

Porting note