doc-next-gen

Mathlib.Algebra.Group.Pi.Lemmas

Module docstring

{"# Extra lemmas about products of monoids and groups

This file proves lemmas about the instances defined in Algebra.Group.Pi.Basic that require more imports. "}

Set.range_one theorem
{α β : Type*} [One β] [Nonempty α] : Set.range (1 : α → β) = { 1 }
Full source 
@[to_additive (attr := simp)]
theorem Set.range_one {α β : Type*} [One β] [Nonempty α] : Set.range (1 : α → β) = {1} :=
  range_const
Range of Constant One Function is Singleton Set $\{1\}$
Informal description
For any nonempty type $\alpha$ and any type $\beta$ with a distinguished element $1 \in \beta$, the range of the constant function $1 : \alpha \to \beta$ is the singleton set $\{1\}$.
Set.preimage_one theorem
{α β : Type*} [One β] (s : Set β) [Decidable ((1 : β) ∈ s)] : (1 : α → β) ⁻¹' s = if (1 : β) ∈ s then Set.univ else ∅
Full source 
@[to_additive]
theorem Set.preimage_one {α β : Type*} [One β] (s : Set β) [Decidable ((1 : β) ∈ s)] :
    (1 : α → β) ⁻¹' s = if (1 : β) ∈ s then Set.univ else ∅ :=
  Set.preimage_const 1 s
Preimage of Constant One Function is Universal or Empty Based on Membership of One
Informal description
For any types $\alpha$ and $\beta$ with a distinguished element $1 \in \beta$, and for any subset $s \subseteq \beta$ with a decidable membership condition for $1$, the preimage of $s$ under the constant function $1 : \alpha \to \beta$ is equal to the universal set $\text{univ}$ if $1 \in s$, and is equal to the empty set $\emptyset$ otherwise. In other words: \[ 1^{-1}(s) = \begin{cases} \text{univ} & \text{if } 1 \in s, \\ \emptyset & \text{otherwise.} \end{cases} \]
Pi.one_mono theorem
[One β] : Monotone (1 : α → β)
Full source 
@[to_additive] lemma one_mono [One β] : Monotone (1 : α → β) := monotone_const
Monotonicity of the Constant One Function
Informal description
For any type $\beta$ with a one element $1$, the constant function $1 : \alpha \to \beta$ is monotone (i.e., order-preserving) with respect to the pointwise order on functions.
Pi.one_anti theorem
[One β] : Antitone (1 : α → β)
Full source 
@[to_additive] lemma one_anti [One β] : Antitone (1 : α → β) := antitone_const
Antitonicity of the Constant One Function
Informal description
For any type $\beta$ with a distinguished element $1$, the constant function $1 : \alpha \to \beta$ is antitone (i.e., order-reversing) with respect to the pointwise order on functions.
MulHom.coe_mul theorem
{M N} {_ : Mul M} {_ : CommSemigroup N} (f g : M →ₙ* N) : (f * g : M → N) = fun x => f x * g x
Full source 
@[to_additive]
theorem coe_mul {M N} {_ : Mul M} {_ : CommSemigroup N} (f g : M →ₙ* N) : (f * g : M → N) =
    fun x => f x * g x := rfl
Pointwise Product of Non-unital Multiplicative Homomorphisms
Informal description
For any multiplicative structure $M$ and commutative semigroup $N$, and for any two non-unital multiplicative homomorphisms $f, g : M \toₙ* N$, the pointwise product $(f * g)(x) = f(x) * g(x)$ holds for all $x \in M$.
Pi.mulHom definition
{γ : Type w} [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) : γ →ₙ* ∀ i, f i
Full source 
/-- A family of MulHom's `f a : γ →ₙ* β a` defines a MulHom `Pi.mulHom f : γ →ₙ* Π a, β a`
given by `Pi.mulHom f x b = f b x`. -/
@[to_additive (attr := simps)
  "A family of AddHom's `f a : γ → β a` defines an AddHom `Pi.addHom f : γ → Π a, β a` given by
  `Pi.addHom f x b = f b x`."]
def Pi.mulHom {γ : Type w} [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) : γ →ₙ* ∀ i, f i where
  toFun x i := g i x
  map_mul' x y := funext fun i => (g i).map_mul x y
Product of non-unital multiplicative homomorphisms
Informal description
Given a family of non-unital multiplicative homomorphisms $g_i : \gamma \to f_i$ for each index $i$, the function $\text{Pi.mulHom}\, g : \gamma \to \prod_i f_i$ is defined by $(\text{Pi.mulHom}\, g)(x)_i = g_i(x)$. This function is itself a non-unital multiplicative homomorphism.
Pi.mulHom_injective theorem
{γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.mulHom g)
Full source 
@[to_additive]
theorem Pi.mulHom_injective {γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i)
    (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.mulHom g) := fun _ _ h =>
  let ⟨i⟩ := ‹Nonempty I›
  hg i ((funext_iff.mp h :) i)
Injectivity of Product of Non-unital Multiplicative Homomorphisms
Informal description
Let $I$ be a nonempty index set, and for each $i \in I$, let $f_i$ and $\gamma$ be multiplicative structures. Given a family of injective non-unital multiplicative homomorphisms $g_i \colon \gamma \to f_i$ for each $i \in I$, the product homomorphism $\prod_i g_i \colon \gamma \to \prod_i f_i$ defined by $(\prod_i g_i)(x)_i = g_i(x)$ is also injective.
Pi.monoidHom definition
{γ : Type w} [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i) : γ →* ∀ i, f i
Full source 
/-- A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism
`Pi.monoidHom f : γ →* Π a, β a` given by `Pi.monoidHom f x b = f b x`. -/
@[to_additive (attr := simps)
  "A family of additive monoid homomorphisms `f a : γ →+ β a` defines a monoid homomorphism
  `Pi.addMonoidHom f : γ →+ Π a, β a` given by `Pi.addMonoidHom f x b = f b x`."]
def Pi.monoidHom {γ : Type w} [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i) :
    γ →* ∀ i, f i :=
  { Pi.mulHom fun i => (g i).toMulHom with
    toFun := fun x i => g i x
    map_one' := funext fun i => (g i).map_one }
Product of monoid homomorphisms
Informal description
Given a family of monoid homomorphisms \( g_i \colon \gamma \to f_i \) for each index \( i \), the function \( \text{Pi.monoidHom}\, g \colon \gamma \to \prod_i f_i \) defined by \( (\text{Pi.monoidHom}\, g)(x)_i = g_i(x) \) is a monoid homomorphism. This construction preserves the multiplicative identity, i.e., \( (\text{Pi.monoidHom}\, g)(1)_i = 1 \) for all \( i \).
Pi.monoidHom_injective theorem
{γ : Type w} [Nonempty I] [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i) (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.monoidHom g)
Full source 
@[to_additive]
theorem Pi.monoidHom_injective {γ : Type w} [Nonempty I] [∀ i, MulOneClass (f i)] [MulOneClass γ]
    (g : ∀ i, γ →* f i) (hg : ∀ i, Function.Injective (g i)) :
    Function.Injective (Pi.monoidHom g) :=
  Pi.mulHom_injective (fun i => (g i).toMulHom) hg
Injectivity of Product of Monoid Homomorphisms
Informal description
Let $I$ be a nonempty index set, and for each $i \in I$, let $f_i$ and $\gamma$ be monoids (equipped with multiplication and identity). Given a family of injective monoid homomorphisms $g_i \colon \gamma \to f_i$ for each $i \in I$, the product homomorphism $\prod_i g_i \colon \gamma \to \prod_i f_i$ defined by $(\prod_i g_i)(x)_i = g_i(x)$ is also injective.
Pi.evalMulHom definition
(i : I) : (∀ i, f i) →ₙ* f i
Full source 
/-- Evaluation of functions into an indexed collection of semigroups at a point is a semigroup
homomorphism.
This is `Function.eval i` as a `MulHom`. -/
@[to_additive (attr := simps)
  "Evaluation of functions into an indexed collection of additive semigroups at a point is an
  additive semigroup homomorphism. This is `Function.eval i` as an `AddHom`."]
def Pi.evalMulHom (i : I) : (∀ i, f i) →ₙ* f i where
  toFun g := g i
  map_mul' _ _ := Pi.mul_apply _ _ i
Evaluation multiplicative homomorphism at index $i$
Informal description
For a family of multiplicative structures $(f_i)_{i \in I}$ and a fixed index $i \in I$, the evaluation map at $i$ is a non-unital multiplicative homomorphism from the product $\prod_{i \in I} f_i$ to $f_i$. Specifically, the map sends a function $g$ to its value $g(i)$, and preserves multiplication.
Pi.constMulHom definition
(α β : Type*) [Mul β] : β →ₙ* α → β
Full source 
/-- `Function.const` as a `MulHom`. -/
@[to_additive (attr := simps) "`Function.const` as an `AddHom`."]
def Pi.constMulHom (α β : Type*) [Mul β] :
    β →ₙ* α → β where
  toFun := Function.const α
  map_mul' _ _ := rfl
Constant multiplicative homomorphism
Informal description
The function `Pi.constMulHom` maps an element $b$ of a multiplicative structure $\beta$ to the constant function $\alpha \to \beta$ that always returns $b$. This mapping preserves multiplication, meaning that for any $b_1, b_2 \in \beta$, the constant function corresponding to $b_1 \cdot b_2$ is equal to the product of the constant functions corresponding to $b_1$ and $b_2$.
MulHom.coeFn definition
(α β : Type*) [Mul α] [CommSemigroup β] : (α →ₙ* β) →ₙ* α → β
Full source 
/-- Coercion of a `MulHom` into a function is itself a `MulHom`.

See also `MulHom.eval`. -/
@[to_additive (attr := simps) "Coercion of an `AddHom` into a function is itself an `AddHom`.

See also `AddHom.eval`."]
def MulHom.coeFn (α β : Type*) [Mul α] [CommSemigroup β] :
    (α →ₙ* β) →ₙ* α → β where
  toFun g := g
  map_mul' _ _ := rfl
Coefficient function as a multiplicative homomorphism
Informal description
The function `MulHom.coeFn` maps a multiplicative homomorphism $g$ from a multiplicative structure $\alpha$ to a commutative semigroup $\beta$ to its underlying function $g : \alpha \to \beta$. This mapping itself is a multiplicative homomorphism, meaning that the pointwise product of two homomorphisms corresponds to the product of their underlying functions.
MulHom.compLeft definition
{α β : Type*} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type*) : (I → α) →ₙ* I → β
Full source 
/-- Semigroup homomorphism between the function spaces `I → α` and `I → β`, induced by a semigroup
homomorphism `f` between `α` and `β`. -/
@[to_additive (attr := simps) "Additive semigroup homomorphism between the function spaces `I → α`
and `I → β`, induced by an additive semigroup homomorphism `f` between `α` and `β`"]
protected def MulHom.compLeft {α β : Type*} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type*) :
    (I → α) →ₙ* I → β where
  toFun h := f ∘ h
  map_mul' _ _ := by ext; simp
Post-composition of non-unital multiplicative homomorphism on function spaces
Informal description
Given a non-unital multiplicative homomorphism $f \colon \alpha \to \beta$ between multiplicative structures $\alpha$ and $\beta$, and a type $I$, the function `MulHom.compLeft` constructs a non-unital multiplicative homomorphism from the function space $I \to \alpha$ to $I \to \beta$ by post-composing with $f$. Explicitly, it maps a function $h \colon I \to \alpha$ to the composition $f \circ h \colon I \to \beta$.
Pi.evalMonoidHom definition
(i : I) : (∀ i, f i) →* f i
Full source 
/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
homomorphism.
This is `Function.eval i` as a `MonoidHom`. -/
@[to_additive (attr := simps) "Evaluation of functions into an indexed collection of additive
monoids at a point is an additive monoid homomorphism. This is `Function.eval i` as an
`AddMonoidHom`."]
def Pi.evalMonoidHom (i : I) : (∀ i, f i) →* f i where
  toFun g := g i
  map_one' := Pi.one_apply i
  map_mul' _ _ := Pi.mul_apply _ _ i
Evaluation homomorphism for product of monoids
Informal description
For a family of monoids $(f_i)_{i \in I}$, the evaluation map at index $i$ is a monoid homomorphism from the product monoid $\prod_{i \in I} f_i$ to $f_i$. Specifically, it maps a function $g$ in the product to its value $g(i)$ at index $i$, preserving the multiplicative identity and the multiplication operation.
Pi.constMonoidHom definition
(α β : Type*) [MulOneClass β] : β →* α → β
Full source 
/-- `Function.const` as a `MonoidHom`. -/
@[to_additive (attr := simps) "`Function.const` as an `AddMonoidHom`."]
def Pi.constMonoidHom (α β : Type*) [MulOneClass β] : β →* α → β where
  toFun := Function.const α
  map_one' := rfl
  map_mul' _ _ := rfl
Constant function as a monoid homomorphism
Informal description
The monoid homomorphism version of the constant function, which maps an element $b$ of a monoid $\beta$ to the constant function $\alpha \to \beta$ that always returns $b$. This homomorphism preserves the multiplicative identity and the multiplication operation.
MonoidHom.coeFn definition
(α β : Type*) [MulOneClass α] [CommMonoid β] : (α →* β) →* α → β
Full source 
/-- Coercion of a `MonoidHom` into a function is itself a `MonoidHom`.

See also `MonoidHom.eval`. -/
@[to_additive (attr := simps) "Coercion of an `AddMonoidHom` into a function is itself
an `AddMonoidHom`.

See also `AddMonoidHom.eval`."]
def MonoidHom.coeFn (α β : Type*) [MulOneClass α] [CommMonoid β] : (α →* β) →* α → β where
  toFun g := g
  map_one' := rfl
  map_mul' _ _ := rfl
Coercion of monoid homomorphisms as a monoid homomorphism
Informal description
The function that coerces a monoid homomorphism $g \colon \alpha \to \beta$ (where $\alpha$ is a monoid and $\beta$ is a commutative monoid) into its underlying function is itself a monoid homomorphism. This means the coercion preserves the multiplicative identity and the multiplication operation.
MonoidHom.compLeft definition
{α β : Type*} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type*) : (I → α) →* I → β
Full source 
/-- Monoid homomorphism between the function spaces `I → α` and `I → β`, induced by a monoid
homomorphism `f` between `α` and `β`. -/
@[to_additive (attr := simps)
  "Additive monoid homomorphism between the function spaces `I → α` and `I → β`, induced by an
  additive monoid homomorphism `f` between `α` and `β`"]
protected def MonoidHom.compLeft {α β : Type*} [MulOneClass α] [MulOneClass β] (f : α →* β)
    (I : Type*) : (I → α) →* I → β where
  toFun h := f ∘ h
  map_one' := by ext; dsimp; simp
  map_mul' _ _ := by ext; simp
Post-composition monoid homomorphism on function spaces
Informal description
Given a monoid homomorphism $f \colon \alpha \to \beta$ between monoids $\alpha$ and $\beta$, and a type $I$, the function `MonoidHom.compLeft` constructs a monoid homomorphism from the function space $I \to \alpha$ to $I \to \beta$ by post-composing with $f$. Specifically, it maps any function $h \colon I \to \alpha$ to the composition $f \circ h \colon I \to \beta$.
OneHom.mulSingle definition
[∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i)
Full source 
/-- The one-preserving homomorphism including a single value
into a dependent family of values, as functions supported at a point.

This is the `OneHom` version of `Pi.mulSingle`. -/
@[to_additive
      "The zero-preserving homomorphism including a single value into a dependent family of values,
      as functions supported at a point.

      This is the `ZeroHom` version of `Pi.single`."]
nonrec def OneHom.mulSingle [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i) where
  toFun := mulSingle i
  map_one' := mulSingle_one i
Identity-preserving homomorphism into a product via point support
Informal description
For a family of types $(f_i)_{i \in I}$ each equipped with a distinguished element $1$, the function `OneHom.mulSingle` takes an index $i \in I$ and constructs an identity-preserving homomorphism from $f_i$ to the product type $\prod_{i \in I} f_i$. Specifically, it maps an element $x \in f_i$ to the function that is $x$ at index $i$ and $1$ elsewhere. This homomorphism satisfies $\text{OneHom.mulSingle } i \, 1 = 1$ for all $i \in I$.
OneHom.mulSingle_apply theorem
[∀ i, One <| f i] (i : I) (x : f i) : mulSingle f i x = Pi.mulSingle i x
Full source 
@[to_additive (attr := simp)]
theorem OneHom.mulSingle_apply [∀ i, One <| f i] (i : I) (x : f i) :
    mulSingle f i x = Pi.mulSingle i x := rfl
Equality of Identity-Preserving Homomorphism and Multiplicative Single Function
Informal description
For a family of types $(f_i)_{i \in I}$ each equipped with a distinguished element $1$, the identity-preserving homomorphism $\text{mulSingle } f \, i \colon f_i \to \prod_{i \in I} f_i$ satisfies $\text{mulSingle } f \, i \, x = \text{Pi.mulSingle } i \, x$ for any $x \in f_i$, where $\text{Pi.mulSingle } i \, x$ is the function that equals $x$ at index $i$ and $1$ elsewhere.
MonoidHom.mulSingle definition
[∀ i, MulOneClass <| f i] (i : I) : f i →* ∀ i, f i
Full source 
/-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
as functions supported at a point.

This is the `MonoidHom` version of `Pi.mulSingle`. -/
@[to_additive
      "The additive monoid homomorphism including a single additive monoid into a dependent family
      of additive monoids, as functions supported at a point.

      This is the `AddMonoidHom` version of `Pi.single`."]
def MonoidHom.mulSingle [∀ i, MulOneClass <| f i] (i : I) : f i →* ∀ i, f i :=
  { OneHom.mulSingle f i with map_mul' := mulSingle_op₂ (fun _ => (· * ·)) (fun _ => one_mul _) _ }
Monoid homomorphism into a product via point support
Informal description
For a family of monoids $(f_i)_{i \in I}$, the function `MonoidHom.mulSingle` takes an index $i \in I$ and constructs a monoid homomorphism from $f_i$ to the product monoid $\prod_{i \in I} f_i$. Specifically, it maps an element $x \in f_i$ to the function that is $x$ at index $i$ and the identity element elsewhere. This homomorphism preserves both the multiplicative structure and the identity element.
MonoidHom.mulSingle_apply theorem
[∀ i, MulOneClass <| f i] (i : I) (x : f i) : mulSingle f i x = Pi.mulSingle i x
Full source 
@[to_additive (attr := simp)]
theorem MonoidHom.mulSingle_apply [∀ i, MulOneClass <| f i] (i : I) (x : f i) :
    mulSingle f i x = Pi.mulSingle i x :=
  rfl
Equality of Monoid Homomorphism and Multiplicative Single Function in Product Monoids
Informal description
For a family of monoids $(f_i)_{i \in I}$, the monoid homomorphism $\text{mulSingle } f \, i \colon f_i \to \prod_{i \in I} f_i$ satisfies $\text{mulSingle } f \, i \, x = \text{Pi.mulSingle } i \, x$ for any $x \in f_i$, where $\text{Pi.mulSingle } i \, x$ is the function that equals $x$ at index $i$ and the identity element $1$ elsewhere.
Pi.mulSingle_sup theorem
[∀ i, SemilatticeSup (f i)] [∀ i, One (f i)] (i : I) (x y : f i) : Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y
Full source 
@[to_additive]
theorem Pi.mulSingle_sup [∀ i, SemilatticeSup (f i)] [∀ i, One (f i)] (i : I) (x y : f i) :
    Pi.mulSingle i (x ⊔ y) = Pi.mulSinglePi.mulSingle i x ⊔ Pi.mulSingle i y :=
  Function.update_sup _ _ _ _
Join Preservation under Multiplicative Single Function in Product Semilattices
Informal description
Let $(f_i)_{i \in I}$ be a family of join-semilattices each equipped with a multiplicative identity $1$. For any index $i \in I$ and elements $x, y \in f_i$, the multiplicative single function satisfies: \[ \text{mulSingle}_i(x \sqcup y) = \text{mulSingle}_i(x) \sqcup \text{mulSingle}_i(y). \] Here, $\text{mulSingle}_i$ is the function that maps $x$ to the element which is $x$ at index $i$ and $1$ elsewhere, and $\sqcup$ denotes the join operation in each $f_i$.
Pi.mulSingle_inf theorem
[∀ i, SemilatticeInf (f i)] [∀ i, One (f i)] (i : I) (x y : f i) : Pi.mulSingle i (x ⊓ y) = Pi.mulSingle i x ⊓ Pi.mulSingle i y
Full source 
@[to_additive]
theorem Pi.mulSingle_inf [∀ i, SemilatticeInf (f i)] [∀ i, One (f i)] (i : I) (x y : f i) :
    Pi.mulSingle i (x ⊓ y) = Pi.mulSinglePi.mulSingle i x ⊓ Pi.mulSingle i y :=
  Function.update_inf _ _ _ _
Meet Preservation for Multiplicative Single Function in Product Semilattices
Informal description
Let $\{f_i\}_{i \in I}$ be a family of meet-semilattices each equipped with a multiplicative identity $1$. For any index $i \in I$ and elements $x, y \in f_i$, the multiplicative single function satisfies: \[ \text{mulSingle}_i (x \sqcap y) = \text{mulSingle}_i x \sqcap \text{mulSingle}_i y. \]
Pi.mulSingle_mul theorem
[∀ i, MulOneClass <| f i] (i : I) (x y : f i) : mulSingle i (x * y) = mulSingle i x * mulSingle i y
Full source 
@[to_additive]
theorem Pi.mulSingle_mul [∀ i, MulOneClass <| f i] (i : I) (x y : f i) :
    mulSingle i (x * y) = mulSingle i x * mulSingle i y :=
  (MonoidHom.mulSingle f i).map_mul x y
Multiplicative Single Function Preserves Multiplication in Product Monoids
Informal description
Let $(f_i)_{i \in I}$ be a family of monoids. For any index $i \in I$ and elements $x, y \in f_i$, the multiplicative single function satisfies: \[ \text{mulSingle}_i(x \cdot y) = \text{mulSingle}_i(x) \cdot \text{mulSingle}_i(y). \] Here, $\text{mulSingle}_i$ is the function that maps $x$ to the element which is $x$ at index $i$ and the identity element $1$ elsewhere, and $\cdot$ denotes the multiplication operation in each $f_i$.
Pi.mulSingle_inv theorem
[∀ i, Group <| f i] (i : I) (x : f i) : mulSingle i x⁻¹ = (mulSingle i x)⁻¹
Full source 
@[to_additive]
theorem Pi.mulSingle_inv [∀ i, Group <| f i] (i : I) (x : f i) :
    mulSingle i x⁻¹ = (mulSingle i x)⁻¹ :=
  (MonoidHom.mulSingle f i).map_inv x
Inverse Preservation for Multiplicative Single Function in Product Groups
Informal description
For any family of groups $(f_i)_{i \in I}$, any index $i \in I$, and any element $x \in f_i$, the multiplicative single function satisfies: \[ \text{mulSingle}_i (x^{-1}) = (\text{mulSingle}_i x)^{-1}. \]
Pi.mulSingle_div theorem
[∀ i, Group <| f i] (i : I) (x y : f i) : mulSingle i (x / y) = mulSingle i x / mulSingle i y
Full source 
@[to_additive]
theorem Pi.mulSingle_div [∀ i, Group <| f i] (i : I) (x y : f i) :
    mulSingle i (x / y) = mulSingle i x / mulSingle i y :=
  (MonoidHom.mulSingle f i).map_div x y
Division Preservation for Multiplicative Single Function in Product Groups
Informal description
For any family of groups $(f_i)_{i \in I}$, any index $i \in I$, and any elements $x, y \in f_i$, the multiplicative single function satisfies: \[ \text{mulSingle}_i(x / y) = \text{mulSingle}_i(x) / \text{mulSingle}_i(y). \] Here, $\text{mulSingle}_i$ is the function that maps $x$ to the element which is $x$ at index $i$ and the identity element $1$ elsewhere, and $/$ denotes the division operation in each $f_i$.
Pi.mulSingle_pow theorem
[∀ i, Monoid (f i)] (i : I) (x : f i) (n : ℕ) : mulSingle i (x ^ n) = mulSingle i x ^ n
Full source 
@[to_additive]
theorem Pi.mulSingle_pow [∀ i, Monoid (f i)] (i : I) (x : f i) (n : ℕ) :
    mulSingle i (x ^ n) = mulSingle i x ^ n :=
  (MonoidHom.mulSingle f i).map_pow x n
Power Law for Multiplicative Single Functions: $\text{mulSingle}_i(x^n) = (\text{mulSingle}_i x)^n$
Informal description
Let $(f_i)_{i \in I}$ be a family of monoids. For any index $i \in I$, element $x \in f_i$, and natural number $n$, the multiplicative single function satisfies: \[ \text{mulSingle}_i(x^n) = (\text{mulSingle}_i x)^n \] where $\text{mulSingle}_i$ is the function that maps $x$ to the element of $\prod_{i \in I} f_i$ which is $x$ at index $i$ and the identity element elsewhere.
Pi.mulSingle_zpow theorem
[∀ i, Group (f i)] (i : I) (x : f i) (n : ℤ) : mulSingle i (x ^ n) = mulSingle i x ^ n
Full source 
@[to_additive]
theorem Pi.mulSingle_zpow [∀ i, Group (f i)] (i : I) (x : f i) (n : ℤ) :
    mulSingle i (x ^ n) = mulSingle i x ^ n :=
  (MonoidHom.mulSingle f i).map_zpow x n
Integer Power Law for Multiplicative Single Functions: $\text{mulSingle}_i(x^n) = (\text{mulSingle}_i x)^n$
Informal description
Let $(f_i)_{i \in I}$ be a family of groups. For any index $i \in I$, element $x \in f_i$, and integer $n$, the multiplicative single function satisfies: \[ \text{mulSingle}_i(x^n) = (\text{mulSingle}_i x)^n \] where $\text{mulSingle}_i$ is the function that maps $x$ to the element of $\prod_{i \in I} f_i$ which is $x$ at index $i$ and the identity element elsewhere.
Pi.mulSingle_commute theorem
[∀ i, MulOneClass <| f i] : Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)
Full source 
/-- The injection into a pi group at different indices commutes.

For injections of commuting elements at the same index, see `Commute.map` -/
@[to_additive
      "The injection into an additive pi group at different indices commutes.

      For injections of commuting elements at the same index, see `AddCommute.map`"]
theorem Pi.mulSingle_commute [∀ i, MulOneClass <| f i] :
    Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y) := by
  intro i j hij x y; ext k
  by_cases h1 : i = k
  · subst h1
    simp [hij]
  by_cases h2 : j = k
  · subst h2
    simp [hij]
  simp [h1, h2]
Commutation of Multiplicative Single Functions at Distinct Indices
Informal description
For any family of multiplicative structures $\{f_i\}_{i \in I}$ where each $f_i$ has a multiplicative identity, the multiplicative single functions at distinct indices commute. That is, for any distinct indices $i, j \in I$ and any elements $x \in f_i$, $y \in f_j$, the elements $\text{mulSingle } i \, x$ and $\text{mulSingle } j \, y$ commute: \[ \text{mulSingle } i \, x \cdot \text{mulSingle } j \, y = \text{mulSingle } j \, y \cdot \text{mulSingle } i \, x. \]
Pi.mulSingle_apply_commute theorem
[∀ i, MulOneClass <| f i] (x : ∀ i, f i) (i j : I) : Commute (mulSingle i (x i)) (mulSingle j (x j))
Full source 
/-- The injection into a pi group with the same values commutes. -/
@[to_additive "The injection into an additive pi group with the same values commutes."]
theorem Pi.mulSingle_apply_commute [∀ i, MulOneClass <| f i] (x : ∀ i, f i) (i j : I) :
    Commute (mulSingle i (x i)) (mulSingle j (x j)) := by
  obtain rfl | hij := Decidable.eq_or_ne i j
  · rfl
  · exact Pi.mulSingle_commute hij _ _
Commutation of Multiplicative Single Functions Applied to a Common Function
Informal description
Let $I$ be an index set and $\{f_i\}_{i \in I}$ be a family of multiplicative structures with identity. For any function $x : \prod_{i \in I} f_i$ and any indices $i, j \in I$, the multiplicative single functions $\text{mulSingle } i \, (x i)$ and $\text{mulSingle } j \, (x j)$ commute, i.e., \[ \text{mulSingle } i \, (x i) \cdot \text{mulSingle } j \, (x j) = \text{mulSingle } j \, (x j) \cdot \text{mulSingle } i \, (x i). \]
Pi.update_eq_div_mul_mulSingle theorem
[∀ i, Group <| f i] (g : ∀ i : I, f i) (x : f i) : Function.update g i x = g / mulSingle i (g i) * mulSingle i x
Full source 
@[to_additive]
theorem Pi.update_eq_div_mul_mulSingle [∀ i, Group <| f i] (g : ∀ i : I, f i) (x : f i) :
    Function.update g i x = g / mulSingle i (g i) * mulSingle i x := by
  ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [Function.update_of_ne h.symm, h]
Function Update Decomposition in Product of Groups: $\text{update } g \, i \, x = g / \text{mulSingle } i \, (g i) \cdot \text{mulSingle } i \, x$
Informal description
Let $I$ be an index set and $\{f_i\}_{i \in I}$ be a family of groups. For any function $g : \prod_{i \in I} f_i$ and any element $x \in f_i$, the function update of $g$ at index $i$ with value $x$ can be expressed as: \[ \text{update } g \, i \, x = g \cdot (\text{mulSingle } i \, (g i))^{-1} \cdot \text{mulSingle } i \, x \] where $\text{mulSingle } i \, y$ denotes the function that is $y$ at $i$ and $1$ elsewhere, and $/$ denotes pointwise division in the product group.
Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle theorem
{M : Type*} [CommMonoid M] {k l m n : I} {u v : M} (hu : u ≠ 1) (hv : v ≠ 1) : (mulSingle k u : I → M) * mulSingle l v = mulSingle m u * mulSingle n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Full source 
@[to_additive]
theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommMonoid M]
    {k l m n : I} {u v : M} (hu : u ≠ 1) (hv : v ≠ 1) :
    (mulSingle k u : I → M) * mulSingle l v = mulSingle m u * mulSingle n v ↔
      k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n := by
  refine ⟨fun h => ?_, ?_⟩
  · have hk := congr_fun h k
    have hl := congr_fun h l
    have hm := (congr_fun h m).symm
    have hn := (congr_fun h n).symm
    simp only [mul_apply, mulSingle_apply, if_pos rfl] at hk hl hm hn
    rcases eq_or_ne k m with (rfl | hkm)
    · refine Or.inl ⟨rfl, not_ne_iff.mp fun hln => (hv ?_).elim⟩
      rcases eq_or_ne k l with (rfl | hkl)
      · rwa [if_neg hln.symm, if_neg hln.symm, one_mul, one_mul] at hn
      · rwa [if_neg hkl.symm, if_neg hln, one_mul, one_mul] at hl
    · rcases eq_or_ne m n with (rfl | hmn)
      · rcases eq_or_ne k l with (rfl | hkl)
        · rw [if_neg hkm.symm, if_neg hkm.symm, one_mul, if_pos rfl] at hm
          exact Or.inr (Or.inr ⟨hm, rfl, rfl⟩)
        · simp only [if_neg hkm, if_neg hkl, mul_one] at hk
          dsimp at hk
          contradiction
      · rw [if_neg hkm.symm, if_neg hmn, one_mul, mul_one] at hm
        obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hm.symm hu)).1
        rw [if_neg hkm, if_neg hkm, one_mul, mul_one] at hk
        obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hk.symm hu)).1
        exact Or.inr (Or.inl ⟨hk.trans (if_pos rfl), rfl, rfl⟩)
  · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨h, rfl, rfl⟩)
    · rfl
    · apply mul_comm
    · simp_rw [← Pi.mulSingle_mul, h, mulSingle_one]
Equivalence of Multiplicative Single Function Products in Commutative Monoids
Informal description
Let $M$ be a commutative monoid, $I$ an index set, and $k, l, m, n \in I$ indices. For elements $u, v \in M$ with $u \neq 1$ and $v \neq 1$, the following are equivalent: 1. The product of the multiplicative single functions $\text{mulSingle}_k(u)$ and $\text{mulSingle}_l(v)$ equals the product of $\text{mulSingle}_m(u)$ and $\text{mulSingle}_n(v)$. 2. Either: - $k = m$ and $l = n$, or - $u = v$, $k = n$, and $l = m$, or - $u \cdot v = 1$, $k = l$, and $m = n$.
SemiconjBy.pi theorem
{x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z i)) : SemiconjBy x y z
Full source 
@[to_additive]
theorem SemiconjBy.pi {x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z i)) :
    SemiconjBy x y z :=
  funext h
Pointwise Semiconjugacy of Functions in Product Structure
Informal description
Let $I$ be an index set and $f : I \to \text{Type}$ be a family of types equipped with multiplication operations. For any three functions $x, y, z : \prod_{i \in I} f(i)$, if for each $i \in I$ the elements $x(i)$, $y(i)$, and $z(i)$ satisfy the semiconjugacy relation $x(i) \cdot y(i) = z(i) \cdot x(i)$, then the functions $x$, $y$, and $z$ satisfy the semiconjugacy relation $x \cdot y = z \cdot x$ pointwise.
Pi.semiconjBy_iff theorem
{x y z : ∀ i, f i} : SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i)
Full source 
@[to_additive]
theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} :
    SemiconjBySemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := funext_iff
Semiconjugacy Relation in Product of Monoids/Groups is Componentwise
Informal description
For functions $x, y, z : \prod_{i} f_i$, the relation $\text{SemiconjBy}\,x\,y\,z$ holds if and only if for every index $i$, the relation $\text{SemiconjBy}\,(x_i)\,(y_i)\,(z_i)$ holds in the component $f_i$.
Commute.pi theorem
{x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y
Full source 
@[to_additive]
theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := SemiconjBy.pi h
Pointwise Commutation in Product of Monoids/Groups
Informal description
Let $I$ be an index set and $f : I \to \text{Type}$ be a family of types equipped with multiplication operations. For any two functions $x, y : \prod_{i \in I} f(i)$, if for each $i \in I$ the elements $x(i)$ and $y(i)$ commute (i.e., $x(i) \cdot y(i) = y(i) \cdot x(i)$), then the functions $x$ and $y$ commute pointwise (i.e., $x \cdot y = y \cdot x$).
Pi.commute_iff theorem
{x y : ∀ i, f i} : Commute x y ↔ ∀ i, Commute (x i) (y i)
Full source 
@[to_additive]
theorem Pi.commute_iff {x y : ∀ i, f i} : CommuteCommute x y ↔ ∀ i, Commute (x i) (y i) := semiconjBy_iff
Commutation in Product of Monoids/Groups is Componentwise
Informal description
For any two elements $x$ and $y$ in the product of monoids/groups $\prod_{i} f_i$, the elements $x$ and $y$ commute (i.e., $x * y = y * x$) if and only if for every index $i$, the components $x_i$ and $y_i$ commute in $f_i$.
Function.update_one theorem
[∀ i, One (f i)] [DecidableEq I] (i : I) : update (1 : ∀ i, f i) i 1 = 1
Full source 
@[to_additive (attr := simp)]
theorem update_one [∀ i, One (f i)] [DecidableEq I] (i : I) : update (1 : ∀ i, f i) i 1 = 1 :=
  update_eq_self i (1 : (a : I) → f a)
Update Preserves Identity Function in Product of Monoids
Informal description
Let $I$ be a type with decidable equality and let $(f_i)_{i \in I}$ be a family of types each equipped with a multiplicative identity element. For any index $i \in I$, updating the constant function $1$ (which assigns the identity element to each index) at $i$ with the identity element $1$ leaves the function unchanged, i.e., $\text{update } 1 \, i \, 1 = 1$.
Function.update_mul theorem
[∀ i, Mul (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i) (x₂ : f i) : update (f₁ * f₂) i (x₁ * x₂) = update f₁ i x₁ * update f₂ i x₂
Full source 
@[to_additive]
theorem update_mul [∀ i, Mul (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i)
    (x₂ : f i) : update (f₁ * f₂) i (x₁ * x₂) = update f₁ i x₁ * update f₂ i x₂ :=
  funext fun j => (apply_update₂ (fun _ => (· * ·)) f₁ f₂ i x₁ x₂ j).symm
Update Preserves Pointwise Multiplication in Product of Multiplicative Structures
Informal description
Let $I$ be a type with decidable equality and let $(f_i)_{i \in I}$ be a family of types each equipped with a multiplication operation. For any two functions $f_1, f_2 : \prod_{i \in I} f_i$, any index $i \in I$, and any elements $x_1, x_2 \in f_i$, the following equality holds: \[ \text{update } (f_1 \cdot f_2) \, i \, (x_1 \cdot x_2) = (\text{update } f_1 \, i \, x_1) \cdot (\text{update } f_2 \, i \, x_2) \] where $\cdot$ denotes pointwise multiplication and $\text{update}$ denotes the function update operation.
Function.update_inv theorem
[∀ i, Inv (f i)] [DecidableEq I] (f₁ : ∀ i, f i) (i : I) (x₁ : f i) : update f₁⁻¹ i x₁⁻¹ = (update f₁ i x₁)⁻¹
Full source 
@[to_additive]
theorem update_inv [∀ i, Inv (f i)] [DecidableEq I] (f₁ : ∀ i, f i) (i : I) (x₁ : f i) :
    update f₁⁻¹ i x₁⁻¹ = (update f₁ i x₁)⁻¹ :=
  funext fun j => (apply_update (fun _ => Inv.inv) f₁ i x₁ j).symm
Update Preserves Pointwise Inversion in Product of Invertible Structures
Informal description
Let $I$ be a type with decidable equality and let $(f_i)_{i \in I}$ be a family of types each equipped with an inversion operation. For any function $f_1 : \prod_{i \in I} f_i$, any index $i \in I$, and any element $x_1 \in f_i$, the following equality holds: \[ \text{update } (f_1^{-1}) \, i \, (x_1^{-1}) = (\text{update } f_1 \, i \, x_1)^{-1} \] where $\text{update}$ denotes the function update operation and $^{-1}$ denotes the pointwise inversion.
Function.update_div theorem
[∀ i, Div (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i) (x₂ : f i) : update (f₁ / f₂) i (x₁ / x₂) = update f₁ i x₁ / update f₂ i x₂
Full source 
@[to_additive]
theorem update_div [∀ i, Div (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i)
    (x₂ : f i) : update (f₁ / f₂) i (x₁ / x₂) = update f₁ i x₁ / update f₂ i x₂ :=
  funext fun j => (apply_update₂ (fun _ => (· / ·)) f₁ f₂ i x₁ x₂ j).symm
Update Preserves Pointwise Division in Product of Divisible Structures
Informal description
Let $I$ be a type with decidable equality and let $(f_i)_{i \in I}$ be a family of types each equipped with a division operation. For any two functions $f_1, f_2 : \prod_{i \in I} f_i$, any index $i \in I$, and any elements $x_1, x_2 \in f_i$, the following equality holds: \[ \text{update } (f_1 / f_2) \, i \, (x_1 / x_2) = (\text{update } f_1 \, i \, x_1) / (\text{update } f_2 \, i \, x_2) \] where $\text{update}$ denotes the function update operation and $/$ denotes pointwise division.
Function.const_eq_one theorem
: const ι a = 1 ↔ a = 1
Full source 
@[to_additive (attr := simp)]
theorem const_eq_one : constconst ι a = 1 ↔ a = 1 :=
  @const_inj _ _ _ _ 1
Constant Function Equals One if and Only if Value Equals One
Informal description
For any type $\iota$ and any element $a$ in a type with a multiplicative identity $1$, the constant function $\mathrm{const}_\iota a$ is equal to the constant function $\mathrm{const}_\iota 1$ if and only if $a = 1$. That is: \[ \mathrm{const}_\iota a = 1 \leftrightarrow a = 1. \]
Function.const_ne_one theorem
: const ι a ≠ 1 ↔ a ≠ 1
Full source 
@[to_additive]
theorem const_ne_one : constconst ι a ≠ 1const ι a ≠ 1 ↔ a ≠ 1 :=
  Iff.not const_eq_one
Constant Function Not Equal to One if and Only if Value Not Equal to One
Informal description
For any type $\iota$ and any element $a$ in a type with a multiplicative identity $1$, the constant function $\mathrm{const}_\iota a$ is not equal to the constant function $\mathrm{const}_\iota 1$ if and only if $a \neq 1$. That is: \[ \mathrm{const}_\iota a \neq 1 \leftrightarrow a \neq 1. \]
Set.piecewise_mul theorem
[∀ i, Mul (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : ∀ i, f i) : s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂
Full source 
@[to_additive]
theorem Set.piecewise_mul [∀ i, Mul (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)]
    (f₁ f₂ g₁ g₂ : ∀ i, f i) :
    s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂ :=
  s.piecewise_op₂ f₁ _ _ _ fun _ => (· * ·)
Piecewise Multiplication of Functions over a Set
Informal description
Let $I$ be a type, and for each $i \in I$, let $f_i$ be a type equipped with a multiplication operation. Given a set $s \subseteq I$ with decidable membership, and functions $f_1, f_2, g_1, g_2 : \forall i, f_i$, the piecewise product function defined by: \[ i \mapsto \begin{cases} f_1(i) \cdot f_2(i) & \text{if } i \in s, \\ g_1(i) \cdot g_2(i) & \text{otherwise,} \end{cases} \] is equal to the product of the piecewise functions: \[ i \mapsto (s.\text{piecewise}\, f_1\, g_1)(i) \cdot (s.\text{piecewise}\, f_2\, g_2)(i). \]
Set.piecewise_inv theorem
[∀ i, Inv (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ g₁ : ∀ i, f i) : s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
Full source 
@[to_additive]
theorem Set.piecewise_inv [∀ i, Inv (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ g₁ : ∀ i, f i) :
    s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹ :=
  s.piecewise_op f₁ g₁ fun _ x => x⁻¹
Inversion Commutes with Piecewise Definition
Informal description
For a set $s \subseteq I$ and functions $f_1, g_1 : \forall i, f i$ where each $f i$ has an inversion operation, the piecewise-defined inversion of $f_1$ and $g_1$ over $s$ is equal to the inversion of the piecewise-defined function of $f_1$ and $g_1$ over $s$. That is, \[ s.\text{piecewise}\, f_1^{-1}\, g_1^{-1} = (s.\text{piecewise}\, f_1\, g_1)^{-1}. \]
Set.piecewise_div theorem
[∀ i, Div (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : ∀ i, f i) : s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
Full source 
@[to_additive]
theorem Set.piecewise_div [∀ i, Div (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)]
    (f₁ f₂ g₁ g₂ : ∀ i, f i) :
    s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂ :=
  s.piecewise_op₂ f₁ _ _ _ fun _ => (· / ·)
Piecewise Division Formula: $s.\text{piecewise}\, (f_1 / f_2)\, (g_1 / g_2) = (s.\text{piecewise}\, f_1\, g_1) / (s.\text{piecewise}\, f_2\, g_2)$
Informal description
Let $I$ be a type, and for each $i \in I$, let $f(i)$ be a type equipped with a division operation. Given a subset $s \subseteq I$ with decidable membership, and functions $f_1, f_2, g_1, g_2 : \forall i, f(i)$, the piecewise division function satisfies: \[ s.\text{piecewise}\, (f_1 / f_2)\, (g_1 / g_2) = (s.\text{piecewise}\, f_1\, g_1) / (s.\text{piecewise}\, f_2\, g_2). \] Here, the piecewise function is defined as: \[ (s.\text{piecewise}\, f\, g)(i) = \begin{cases} f(i) & \text{if } i \in s, \\ g(i) & \text{otherwise.} \end{cases} \]
Function.ExtendByOne.hom definition
[MulOneClass R] : (ι → R) →* η → R
Full source 
/-- `Function.extend s f 1` as a bundled hom. -/
@[to_additive (attr := simps) Function.ExtendByZero.hom "`Function.extend s f 0` as a bundled hom."]
noncomputable def Function.ExtendByOne.hom [MulOneClass R] :
    (ι → R) →* η → R where
  toFun f := Function.extend s f 1
  map_one' := Function.extend_one s
  map_mul' f g := by simpa using Function.extend_mul s f g 1 1
Monoid Homomorphism Extension by One
Informal description
Given a monoid $R$ and a function $s : \iota \to \eta$, the function $\text{ExtendByOne.hom}$ maps a function $f : \iota \to R$ to the monoid homomorphism $\eta \to R$ defined by extending $f$ along $s$ with the default value $1$ (the identity of $R$). Specifically, for any $y \in \eta$, if there exists $x \in \iota$ such that $s(x) = y$, then $\text{ExtendByOne.hom}\,f\,y = f(x)$; otherwise, $\text{ExtendByOne.hom}\,f\,y = 1$. This construction ensures that $\text{ExtendByOne.hom}$ preserves the monoid structure, i.e., it maps the identity function to the identity homomorphism and preserves multiplication pointwise.
Pi.mulSingle_mono theorem
: Monotone (Pi.mulSingle i : f i → ∀ i, f i)
Full source 
@[to_additive]
theorem mulSingle_mono : Monotone (Pi.mulSingle i : f i → ∀ i, f i) :=
  Function.update_mono
Monotonicity of Multiplicative Single Function in Product Space
Informal description
For any index $i$, the function $\mathrm{mulSingle}_i : f(i) \to \prod_{i} f(i)$, which maps $x$ to the function that is $x$ at $i$ and $1$ elsewhere, is monotone. That is, if $x \leq y$ in $f(i)$, then $\mathrm{mulSingle}_i(x) \leq \mathrm{mulSingle}_i(y)$ in the product space $\prod_{i} f(i)$.
Pi.mulSingle_strictMono theorem
: StrictMono (Pi.mulSingle i : f i → ∀ i, f i)
Full source 
@[to_additive]
theorem mulSingle_strictMono : StrictMono (Pi.mulSingle i : f i → ∀ i, f i) :=
  Function.update_strictMono
Strict Monotonicity of Multiplicative Single Function
Informal description
For any index $i$, the function $\mathrm{mulSingle}_i : f(i) \to \prod_{i} f(i)$, which maps $x$ to the function that is $x$ at $i$ and $1$ elsewhere, is strictly monotone. That is, if $x < y$ in $f(i)$, then $\mathrm{mulSingle}_i(x) < \mathrm{mulSingle}_i(y)$ in the product space $\prod_{i} f(i)$.
Pi.mulSingle_comp_equiv theorem
{m n : Type*} [DecidableEq n] [DecidableEq m] [One α] (σ : n ≃ m) (i : m) (x : α) : Pi.mulSingle i x ∘ σ = Pi.mulSingle (σ.symm i) x
Full source 
@[to_additive]
lemma mulSingle_comp_equiv {m n : Type*} [DecidableEq n] [DecidableEq m] [One α] (σ : n ≃ m)
    (i : m) (x : α) : Pi.mulSinglePi.mulSingle i x ∘ σ = Pi.mulSingle (σ.symm i) x := by
  ext x
  aesop (add simp Pi.mulSingle_apply)
Composition of Multiplicative Single Function with Equivalence
Informal description
Let $m$ and $n$ be types with decidable equality, and let $\alpha$ be a type with a multiplicative identity $1$. For any equivalence $\sigma : n \simeq m$, any index $i \in m$, and any element $x \in \alpha$, the composition of the multiplicative single function $\text{mulSingle}_i(x) : m \to \alpha$ with $\sigma$ is equal to the multiplicative single function $\text{mulSingle}_{\sigma^{-1}(i)}(x) : n \to \alpha$. That is, \[ \text{mulSingle}_i(x) \circ \sigma = \text{mulSingle}_{\sigma^{-1}(i)}(x). \]
Sigma.curry_one theorem
[∀ a b, One (γ a b)] : Sigma.curry (1 : (i : Σ a, β a) → γ i.1 i.2) = 1
Full source 
@[to_additive (attr := simp)]
theorem curry_one [∀ a b, One (γ a b)] : Sigma.curry (1 : (i : Σ a, β a) → γ i.1 i.2) = 1 :=
  rfl
Curried Constant One Function Equals One
Informal description
For any family of types $\gamma$ indexed by $\alpha$ and $\beta$ where each $\gamma(a,b)$ has a multiplicative identity element, the curried version of the constant one function equals the constant one function. That is, $\mathrm{curry}(1) = 1$.
Sigma.uncurry_one theorem
[∀ a b, One (γ a b)] : Sigma.uncurry (1 : ∀ a b, γ a b) = 1
Full source 
@[to_additive (attr := simp)]
theorem uncurry_one [∀ a b, One (γ a b)] : Sigma.uncurry (1 : ∀ a b, γ a b) = 1 :=
  rfl
Uncurried Constant One Function Equals One
Informal description
For any family of types $\gamma$ indexed by $\alpha$ and $\beta$ where each $\gamma(a,b)$ has a multiplicative identity element, the uncurried version of the constant one function equals the constant one function. That is, $\text{Sigma.uncurry}(1) = 1$.
Sigma.curry_mul theorem
[∀ a b, Mul (γ a b)] (x y : (i : Σ a, β a) → γ i.1 i.2) : Sigma.curry (x * y) = Sigma.curry x * Sigma.curry y
Full source 
@[to_additive (attr := simp)]
theorem curry_mul [∀ a b, Mul (γ a b)] (x y : (i : Σ a, β a) → γ i.1 i.2) :
    Sigma.curry (x * y) = Sigma.curry x * Sigma.curry y :=
  rfl
Currying Preserves Pointwise Multiplication in Sigma Types
Informal description
Let $\gamma$ be a family of types indexed by $\alpha$ and $\beta$ such that for each $a \in \alpha$ and $b \in \beta a$, the type $\gamma a b$ has a multiplication operation. For any two functions $x, y : \Pi (i : \Sigma a, \beta a), \gamma i.1 i.2$, the curried version of their pointwise product equals the pointwise product of their curried versions. That is, \[ \mathrm{curry}(x \cdot y) = \mathrm{curry}(x) \cdot \mathrm{curry}(y). \]
Sigma.uncurry_mul theorem
[∀ a b, Mul (γ a b)] (x y : ∀ a b, γ a b) : Sigma.uncurry (x * y) = Sigma.uncurry x * Sigma.uncurry y
Full source 
@[to_additive (attr := simp)]
theorem uncurry_mul [∀ a b, Mul (γ a b)] (x y : ∀ a b, γ a b) :
    Sigma.uncurry (x * y) = Sigma.uncurry x * Sigma.uncurry y :=
  rfl
Uncurrying Preserves Multiplication of Dependent Functions
Informal description
For any family of types $\gamma$ indexed by $\alpha$ and $\beta$ where each $\gamma(a,b)$ has a multiplication operation, and for any two dependent functions $x, y : \forall a b, \gamma a b$, the uncurried version of their product equals the product of their uncurried versions. That is, $\text{Sigma.uncurry}(x * y) = \text{Sigma.uncurry}(x) * \text{Sigma.uncurry}(y)$.
Sigma.curry_inv theorem
[∀ a b, Inv (γ a b)] (x : (i : Σ a, β a) → γ i.1 i.2) : Sigma.curry (x⁻¹) = (Sigma.curry x)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem curry_inv [∀ a b, Inv (γ a b)] (x : (i : Σ a, β a) → γ i.1 i.2) :
    Sigma.curry (x⁻¹) = (Sigma.curry x)⁻¹ :=
  rfl
Currying Preserves Pointwise Inversion in Sigma Types
Informal description
Let $\gamma$ be a family of types indexed by $\alpha$ and $\beta$ such that for each $a \in \alpha$ and $b \in \beta a$, $\gamma a b$ has an inversion operation. For any function $x : \Sigma a, \beta a \to \gamma a.1 a.2$, the curried version of the pointwise inverse of $x$ equals the pointwise inverse of the curried version of $x$. That is, $\mathrm{curry}(x^{-1}) = (\mathrm{curry}(x))^{-1}$.
Sigma.uncurry_inv theorem
[∀ a b, Inv (γ a b)] (x : ∀ a b, γ a b) : Sigma.uncurry (x⁻¹) = (Sigma.uncurry x)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem uncurry_inv [∀ a b, Inv (γ a b)] (x : ∀ a b, γ a b) :
    Sigma.uncurry (x⁻¹) = (Sigma.uncurry x)⁻¹ :=
  rfl
Uncurrying Commutes with Pointwise Inversion
Informal description
For any family of types $\gamma$ indexed by $\alpha$ and $\beta$ where each $\gamma(a,b)$ has an inversion operation, and for any function $x : \forall a b, \gamma(a,b)$, the uncurried version of the pointwise inverse $x^{-1}$ is equal to the inverse of the uncurried version of $x$. In other words, if we first invert $x$ pointwise and then uncurry, it is the same as first uncurrying $x$ and then inverting the resulting function.
Sigma.curry_mulSingle theorem
[DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)] (i : Σ a, β a) (x : γ i.1 i.2) : Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.1 (Pi.mulSingle i.2 x)
Full source 
@[to_additive (attr := simp)]
theorem curry_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
    (i : Σ a, β a) (x : γ i.1 i.2) :
    Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.1 (Pi.mulSingle i.2 x) := by
  simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]
Currying Commutes with Multiplicative Single Function on Sigma Types
Informal description
Let $\alpha$ be a type with decidable equality, $\beta : \alpha \to \text{Type}$ a family of types with decidable equality for each $\beta(a)$, and $\gamma : \Pi (a : \alpha), \beta(a) \to \text{Type}$ a family of types with a multiplicative identity for each $\gamma(a,b)$. Given an element $i = \langle a, b \rangle \in \Sigma a, \beta(a)$ and a value $x \in \gamma(a,b)$, the curried version of the multiplicative single function $\text{mulSingle}_i x$ is equal to the multiplicative single function at $a$ applied to the multiplicative single function at $b$ applied to $x$. That is: \[ \mathrm{curry}(\text{mulSingle}_i x) = \text{mulSingle}_a (\text{mulSingle}_b x) \]
Sigma.uncurry_mulSingle_mulSingle theorem
[DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)] (a : α) (b : β a) (x : γ a b) : Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle (Sigma.mk a b) x
Full source 
@[to_additive (attr := simp)]
theorem uncurry_mulSingle_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
    (a : α) (b : β a) (x : γ a b) :
    Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle (Sigma.mk a b) x := by
  rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]
Uncurrying of Nested Multiplicative Single Functions on Sigma Types
Informal description
Let $\alpha$ be a type with decidable equality, $\beta : \alpha \to \text{Type}$ a family of types with decidable equality for each $\beta(a)$, and $\gamma : \Pi (a : \alpha), \beta(a) \to \text{Type}$ a family of types with a multiplicative identity for each $\gamma(a,b)$. For any $a \in \alpha$, $b \in \beta(a)$, and $x \in \gamma(a,b)$, the uncurried version of the multiplicative single function at $a$ applied to the multiplicative single function at $b$ applied to $x$ is equal to the multiplicative single function at the pair $\langle a, b \rangle$ applied to $x$. That is: \[ \mathrm{uncurry}(\text{mulSingle}_a (\text{mulSingle}_b x)) = \text{mulSingle}_{\langle a, b \rangle} x \]