Mathlib.Algebra.Group.Units.Defs

Units structure

(α : Type u) [Monoid α]

Full source

/-- Units of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. -/
structure Units (α : Type u) [Monoid α] where
  /-- The underlying value in the base `Monoid`. -/
  val : α
  /-- The inverse value of `val` in the base `Monoid`. -/
  inv : α
  /-- `inv` is the right inverse of `val` in the base `Monoid`. -/
  val_inv : val * inv = 1
  /-- `inv` is the left inverse of `val` in the base `Monoid`. -/
  inv_val : inv * val = 1

Group of units of a monoid

Informal description

The structure representing the group of units (invertible elements) of a monoid $\alpha$. An element $x$ of $\alpha$ is a unit if there exists an element $y$ in $\alpha$ such that $x \cdot y = 1$ and $y \cdot x = 1$. This bundled version includes the inverse element explicitly, allowing it to be computed. The notation $\alpha^\times$ is used for `Units α`, resembling the common mathematical notation for the group of units in a ring.

term_ˣ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
postfix:1024 "ˣ" => Units

Notation for units of a monoid

Informal description

The notation `Mˣ` denotes the group of units (invertible elements) of a monoid `M`. This is analogous to the common mathematical notation $R^{\times}$ for the units of a ring.

AddUnits structure

(α : Type u) [AddMonoid α]

Full source

/-- Units of an `AddMonoid`, bundled version.

An element of an `AddMonoid` is a unit if it has a two-sided additive inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `isAddUnit`. -/
structure AddUnits (α : Type u) [AddMonoid α] where
  /-- The underlying value in the base `AddMonoid`. -/
  val : α
  /-- The additive inverse value of `val` in the base `AddMonoid`. -/
  neg : α
  /-- `neg` is the right additive inverse of `val` in the base `AddMonoid`. -/
  val_neg : val + neg = 0
  /-- `neg` is the left additive inverse of `val` in the base `AddMonoid`. -/
  neg_val : neg + val = 0

Additive Units of an Additive Monoid

Informal description

The structure `AddUnits α` represents the additive units (i.e., invertible elements) of an additive monoid `α`. An element `a` of `α` is an additive unit if there exists another element `b` such that `a + b = 0` and `b + a = 0`. This structure bundles the inverse element `b` so that it can be explicitly computed. For a predicate version (without bundling the inverse), see `IsAddUnit`.

Units.instCoeHead instance

: CoeHead αˣ α

Full source

/-- A unit can be interpreted as a term in the base `Monoid`. -/
@[to_additive "An additive unit can be interpreted as a term in the base `AddMonoid`."]
instance : CoeHead αˣ α :=
  ⟨val⟩

Canonical Inclusion of Units into Monoid

Informal description

For any monoid $\alpha$, there is a canonical way to interpret a unit $u \in \alpha^\times$ as an element of $\alpha$.

Units.instInv instance

: Inv αˣ

Full source

/-- The inverse of a unit in a `Monoid`. -/
@[to_additive "The additive inverse of an additive unit in an `AddMonoid`."]
instance instInv : Inv αˣ :=
  ⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩

Inversion Operation on Units of a Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ has an inversion operation that sends each unit $u$ to its inverse $u^{-1}$.

Units.Simps.val_inv definition

(u : αˣ) : α

Full source

/-- See Note [custom simps projection] -/
@[to_additive "See Note [custom simps projection]"]
def Simps.val_inv (u : αˣ) : α := ↑(u⁻¹)

Underlying element of the inverse of a unit

Informal description

The function maps a unit $ u $ of a monoid $ \alpha $ to the underlying element of its inverse $ u^{-1} $ in $ \alpha $.

Units.val_mk theorem

(a : α) (b h₁ h₂) : ↑(Units.mk a b h₁ h₂) = a

Full source

@[to_additive]
theorem val_mk (a : α) (b h₁ h₂) : ↑(Units.mk a b h₁ h₂) = a :=
  rfl

Underlying Element of Constructed Unit

Informal description

For any elements $a, b$ of a monoid $\alpha$ and proofs $h_1, h_2$ that they are mutual inverses, the underlying element of the unit $\mathrm{mk}(a, b, h_1, h_2)$ is equal to $a$.

Units.ext theorem

: Function.Injective (val : αˣ → α)

Full source

@[to_additive (attr := ext)]
theorem ext : Function.Injective (val : αˣ → α)
  | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
    simp only at e; subst v'; congr
    simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

Injectivity of the Unit Embedding

Informal description

The canonical map from the group of units $\alpha^\times$ to the underlying monoid $\alpha$ is injective. In other words, if two units $u, v \in \alpha^\times$ satisfy $u = v$ as elements of $\alpha$, then $u = v$ as units.

Units.instDecidableEq instance

[DecidableEq α] : DecidableEq αˣ

Full source

/-- Units have decidable equality if the base `Monoid` has decidable equality. -/
@[to_additive "Additive units have decidable equality
if the base `AddMonoid` has deciable equality."]
instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff

Decidable Equality for the Group of Units

Informal description

For any monoid $\alpha$ with decidable equality, the group of units $\alpha^\times$ also has decidable equality.

Units.mk_val theorem

(u : αˣ) (y h₁ h₂) : mk (u : α) y h₁ h₂ = u

Full source

@[to_additive (attr := simp)]
theorem mk_val (u : αˣ) (y h₁ h₂) : mk (u : α) y h₁ h₂ = u :=
  ext rfl

Unit Construction Equals Original Unit

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and for any elements $y, h_1, h_2$ satisfying the unit conditions, the constructed unit $\text{mk}(u, y, h_1, h_2)$ is equal to $u$.

Units.copy definition

(u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑u⁻¹) : αˣ

Full source

/-- Copy a unit, adjusting definition equalities. -/
@[to_additive (attr := simps) "Copy an `AddUnit`, adjusting definitional equalities."]
def copy (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑u⁻¹) : αˣ :=
  { val, inv, inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }

Copy of a unit with adjusted values

Informal description

Given a unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and elements $val$ and $inv$ in $\alpha$ such that $val = u$ and $inv = u^{-1}$, this function constructs a new unit with $val$ as its value and $inv$ as its inverse, ensuring that the unit properties are preserved.

Units.copy_eq theorem

(u : αˣ) (val hv inv hi) : u.copy val hv inv hi = u

Full source

@[to_additive]
theorem copy_eq (u : αˣ) (val hv inv hi) : u.copy val hv inv hi = u :=
  ext hv

Equality of Unit Copy with Original Unit

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and for any elements $val$, $inv$ in $\alpha$ such that $val = u$ and $inv = u^{-1}$, the constructed copy $u.copy\ val\ hv\ inv\ hi$ is equal to $u$.

Units.instMul instance

: Mul αˣ

Full source

/-- Units of a monoid have an induced multiplication. -/
@[to_additive "Additive units of an additive monoid have an induced addition."]
instance : Mul αˣ where
  mul u₁ u₂ :=
    ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
      by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv],
      by rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]⟩

Multiplication Operation on Units of a Monoid

Informal description

The group of units $\alpha^\times$ of a monoid $\alpha$ is equipped with a multiplication operation.

Units.instOne instance

: One αˣ

Full source

/-- Units of a monoid have a unit -/
@[to_additive "Additive units of an additive monoid have a zero."]
instance : One αˣ where
  one := ⟨1, 1, one_mul 1, one_mul 1⟩

Identity Element in the Group of Units

Informal description

The group of units $\alpha^\times$ of a monoid $\alpha$ has a multiplicative identity element.

Units.instMulOneClass instance

: MulOneClass αˣ

Full source

/-- Units of a monoid have a multiplication and multiplicative identity. -/
@[to_additive "Additive units of an additive monoid have an addition and an additive identity."]
instance instMulOneClass : MulOneClass αˣ where
  one_mul u := ext <| one_mul (u : α)
  mul_one u := ext <| mul_one (u : α)

Units Form a MulOneClass

Informal description

The group of units $\alpha^\times$ of a monoid $\alpha$ forms a `MulOneClass`, meaning it is equipped with a multiplication operation and a multiplicative identity element that satisfies the identity laws.

Units.instInhabited instance

: Inhabited αˣ

Full source

/-- Units of a monoid are inhabited because `1` is a unit. -/
@[to_additive "Additive units of an additive monoid are inhabited because `0` is an additive unit."]
instance : Inhabited αˣ :=
  ⟨1⟩

Inhabitedness of the Group of Units in a Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ is inhabited, with the multiplicative identity $1$ being a unit.

Units.instRepr instance

[Repr α] : Repr αˣ

Full source

/-- Units of a monoid have a representation of the base value in the `Monoid`. -/
@[to_additive "Additive units of an additive monoid have a representation of the base value in
the `AddMonoid`."]
instance [Repr α] : Repr αˣ :=
  ⟨reprPrec ∘ val⟩

Representation of Units in a Monoid

Informal description

For any monoid $\alpha$ with a representation of its elements, the group of units $\alpha^\times$ also has a representation, where each unit is represented by its underlying element in $\alpha$.

Units.val_mul theorem

: (↑(a * b) : α) = a * b

Full source

@[to_additive (attr := simp, norm_cast)]
theorem val_mul : (↑(a * b) : α) = a * b :=
  rfl

Canonical Map Preserves Multiplication of Units

Informal description

For any units $a$ and $b$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the canonical map from $\alpha^\times$ to $\alpha$ preserves multiplication, i.e., $(a \cdot b) = a \cdot b$ where the left-hand side is multiplication in $\alpha^\times$ and the right-hand side is multiplication in $\alpha$.

Units.val_one theorem

: ((1 : αˣ) : α) = 1

Full source

@[to_additive (attr := simp, norm_cast)]
theorem val_one : ((1 : αˣ) : α) = 1 :=
  rfl

Identity Preservation in Units Canonical Map

Informal description

The canonical map from the group of units $\alpha^\times$ to the monoid $\alpha$ sends the identity element $1$ of $\alpha^\times$ to the identity element $1$ of $\alpha$.

Units.val_eq_one theorem

{a : αˣ} : (a : α) = 1 ↔ a = 1

Full source

@[to_additive (attr := simp, norm_cast)]
theorem val_eq_one {a : αˣ} : (a : α) = 1 ↔ a = 1 := by rw [← Units.val_one, eq_iff]

Characterization of Unit Identity via Canonical Map: $(a : \alpha) = 1 \leftrightarrow a = 1$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the canonical image of $a$ in $\alpha$ equals the identity element $1$ if and only if $a$ is the identity element of $\alpha^\times$.

Units.inv_mk theorem

(x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁

Full source

@[to_additive (attr := simp)]
theorem inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ :=
  rfl

Inverse of Constructed Unit in a Monoid

Informal description

For any elements $x$ and $y$ in a monoid $\alpha$ such that $x \cdot y = 1$ ($h₁$) and $y \cdot x = 1$ ($h₂$), the inverse of the unit $\text{mk}(x, y, h₁, h₂)$ is equal to $\text{mk}(y, x, h₂, h₁)$.

Units.inv_eq_val_inv theorem

: a.inv = ((a⁻¹ : αˣ) : α)

Full source

@[to_additive (attr := simp)]
theorem inv_eq_val_inv : a.inv = ((a⁻¹ : αˣ) : α) :=
  rfl

Inverse of Unit as Element Equals Coerced Unit Inverse

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the inverse of $a$ as an element of $\alpha$ is equal to the coercion of the inverse of $a$ (considered as a unit) back to $\alpha$. That is, $a^{-1}_{\alpha} = (a^{-1}_{\alpha^\times})_\alpha$.

Units.inv_mul theorem

: (↑a⁻¹ * a : α) = 1

Full source

@[to_additive (attr := simp)]
theorem inv_mul : (↑a⁻¹ * a : α) = 1 :=
  inv_val _

Left inverse property for units: $a^{-1} \cdot a = 1$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the product of the inverse of $a$ (considered as an element of $\alpha$) and $a$ equals the multiplicative identity, i.e., $a^{-1} \cdot a = 1$.

Units.mul_inv theorem

: (a * ↑a⁻¹ : α) = 1

Full source

@[to_additive (attr := simp)]
theorem mul_inv : (a * ↑a⁻¹ : α) = 1 :=
  val_inv _

Unit Multiplication by Inverse Yields Identity

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the product of $a$ and its inverse (considered as an element of $\alpha$) equals the multiplicative identity, i.e., $a \cdot a^{-1} = 1$.

Units.commute_coe_inv theorem

: Commute (a : α) ↑a⁻¹

Full source

@[to_additive] lemma commute_coe_inv : Commute (a : α) ↑a⁻¹ := by
  rw [Commute, SemiconjBy, inv_mul, mul_inv]

Commutation of a Unit with its Inverse

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the element $a$ (considered as an element of $\alpha$) commutes with its inverse $a^{-1}$, i.e., $a \cdot a^{-1} = a^{-1} \cdot a$.

Units.commute_inv_coe theorem

: Commute ↑a⁻¹ (a : α)

Full source

@[to_additive] lemma commute_inv_coe : Commute ↑a⁻¹ (a : α) := a.commute_coe_inv.symm

Commutation of Inverse with Unit: $a^{-1} \cdot a = a \cdot a^{-1}$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the inverse $a^{-1}$ (considered as an element of $\alpha$) commutes with $a$, i.e., $a^{-1} \cdot a = a \cdot a^{-1}$.

Units.inv_mul_of_eq theorem

{a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1

Full source

@[to_additive]
theorem inv_mul_of_eq {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 := by rw [← h, u.inv_mul]

Left inverse property for units with equality condition: $u^{-1} \cdot a = 1$ when $\uparrow u = a$

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$ and any element $a \in \alpha$ such that the underlying element of $u$ equals $a$ (i.e., $\uparrow u = a$), the product of the inverse of $u$ (considered as an element of $\alpha$) and $a$ equals the multiplicative identity, i.e., $\uparrow u^{-1} \cdot a = 1$.

Units.mul_inv_of_eq theorem

{a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1

Full source

@[to_additive]
theorem mul_inv_of_eq {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1 := by rw [← h, u.mul_inv]

Unit Element Multiplied by Inverse Yields Identity

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, if the underlying element of $u$ equals $a$ (i.e., $\uparrow u = a$), then $a$ multiplied by the inverse of $u$ equals the multiplicative identity, i.e., $a \cdot u^{-1} = 1$.

Units.mul_inv_cancel_left theorem

(a : αˣ) (b : α) : (a : α) * (↑a⁻¹ * b) = b

Full source

@[to_additive (attr := simp)]
theorem mul_inv_cancel_left (a : αˣ) (b : α) : (a : α) * (↑a⁻¹ * b) = b := by
  rw [← mul_assoc, mul_inv, one_mul]

Left Cancellation Property for Units: $a \cdot (a^{-1} \cdot b) = b$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$ and any element $b \in \alpha$, the product $a \cdot (a^{-1} \cdot b) = b$.

Units.inv_mul_cancel_left theorem

(a : αˣ) (b : α) : (↑a⁻¹ : α) * (a * b) = b

Full source

@[to_additive (attr := simp)]
theorem inv_mul_cancel_left (a : αˣ) (b : α) : (↑a⁻¹ : α) * (a * b) = b := by
  rw [← mul_assoc, inv_mul, one_mul]

Left cancellation property for units: $a^{-1} \cdot (a \cdot b) = b$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and for any element $b \in \alpha$, the following identity holds: $a^{-1} \cdot (a \cdot b) = b$.

Units.inv_mul_eq_iff_eq_mul theorem

{b c : α} : ↑a⁻¹ * b = c ↔ b = a * c

Full source

@[to_additive]
theorem inv_mul_eq_iff_eq_mul {b c : α} : ↑a⁻¹ * b = c ↔ b = a * c :=
  ⟨fun h => by rw [← h, mul_inv_cancel_left], fun h => by rw [h, inv_mul_cancel_left]⟩

Equivalence of Inverse Multiplication: $a^{-1}b = c \leftrightarrow b = ac$

Informal description

For any unit $a$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and for any elements $b, c \in \alpha$, the equation $a^{-1} \cdot b = c$ holds if and only if $b = a \cdot c$.

Units.instMonoid instance

: Monoid αˣ

Full source

@[to_additive]
instance instMonoid : Monoid αˣ :=
  { (inferInstance : MulOneClass αˣ) with
    mul_assoc := fun _ _ _ => ext <| mul_assoc _ _ _,
    npow := fun n a ↦
      { val := a ^ n
        inv := a⁻¹ ^ n
        val_inv := by rw [← a.commute_coe_inv.mul_pow]; simp
        inv_val := by rw [← a.commute_inv_coe.mul_pow]; simp }
    npow_zero := fun a ↦ by ext; simp
    npow_succ := fun n a ↦ by ext; simp [pow_succ] }

Monoid Structure on Units of a Monoid

Informal description

The group of units $\alpha^\times$ of a monoid $\alpha$ forms a monoid under the multiplication operation inherited from $\alpha$.

Units.instDiv instance

: Div αˣ

Full source

/-- Units of a monoid have division -/
@[to_additive "Additive units of an additive monoid have subtraction."]
instance : Div αˣ where
  div := fun a b ↦
    { val := a * b⁻¹
      inv := b * a⁻¹
      val_inv := by rw [mul_assoc, inv_mul_cancel_left, mul_inv]
      inv_val := by rw [mul_assoc, inv_mul_cancel_left, mul_inv] }

Division Operation on Units of a Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ has a division operation defined by $u / v = u \cdot v^{-1}$ for any units $u, v \in \alpha^\times$.

Units.instDivInvMonoid instance

: DivInvMonoid αˣ

Full source

/-- Units of a monoid form a `DivInvMonoid`. -/
@[to_additive "Additive units of an additive monoid form a `SubNegMonoid`."]
instance instDivInvMonoid : DivInvMonoid αˣ where
  zpow := fun n a ↦ match n, a with
    | Int.ofNat n, a => a ^ n
    | Int.negSucc n, a => (a ^ n.succ)⁻¹
  zpow_zero' := fun a ↦ by simp
  zpow_succ' := fun n a ↦ by simp [pow_succ]
  zpow_neg' := fun n a ↦ by simp

Units of a Monoid Form a Division Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ forms a division monoid, where the division operation is defined by $u / v = u \cdot v^{-1}$ for any units $u, v \in \alpha^\times$.

Units.instGroup instance

: Group αˣ

Full source

/-- Units of a monoid form a group. -/
@[to_additive "Additive units of an additive monoid form an additive group."]
instance instGroup : Group αˣ where
  inv_mul_cancel := fun u => ext u.inv_val

Group Structure on Units of a Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ forms a group, where the group operation is multiplication in $\alpha$, the identity element is $1$, and the inverse of a unit $u$ is its two-sided inverse in $\alpha$.

Units.instCommGroupUnits instance

{α} [CommMonoid α] : CommGroup αˣ

Full source

/-- Units of a commutative monoid form a commutative group. -/
@[to_additive "Additive units of an additive commutative monoid form
an additive commutative group."]
instance instCommGroupUnits {α} [CommMonoid α] : CommGroup αˣ where
  mul_comm := fun _ _ => ext <| mul_comm _ _

Commutative Group Structure on Units of a Commutative Monoid

Informal description

For any commutative monoid $\alpha$, the group of units $\alpha^\times$ forms a commutative group, where the group operation is multiplication in $\alpha$, the identity element is $1$, and the inverse of a unit $u$ is its two-sided inverse in $\alpha$.

Units.val_pow_eq_pow_val theorem

(n : ℕ) : ↑(a ^ n) = (a ^ n : α)

Full source

@[to_additive (attr := simp, norm_cast)]
lemma val_pow_eq_pow_val (n : ℕ) : ↑(a ^ n) = (a ^ n : α) := rfl

Power of Unit Coincides with Power in Base Monoid

Informal description

For any unit $a$ in a monoid $\alpha$ and any natural number $n$, the canonical inclusion map $\alpha^\times \to \alpha$ satisfies $(a^n) = (a)^n$, where the left-hand side is the $n$-th power in the group of units $\alpha^\times$ and the right-hand side is the $n$-th power in $\alpha$.

Units.val_inv_eq_inv_val theorem

(u : αˣ) : ↑u⁻¹ = (u⁻¹ : α)

Full source

@[to_additive (attr := simp, norm_cast)] lemma val_inv_eq_inv_val (u : αˣ) : ↑u⁻¹ = (u⁻¹ : α) :=
  Eq.symm <| inv_eq_of_mul_eq_one_right u.mul_inv

Coercion of Unit Inverse Equals Inverse of Coercion

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the coercion of the inverse $u^{-1}$ to $\alpha$ equals the inverse of the coercion of $u$ to $\alpha$, i.e., $u^{-1} = (u)^{-1}$ in $\alpha$.

Units.val_div_eq_div_val theorem

: ∀ u₁ u₂ : αˣ, ↑(u₁ / u₂) = (u₁ / u₂ : α)

Full source

@[to_additive (attr := simp, norm_cast)]
lemma val_div_eq_div_val : ∀ u₁ u₂ : αˣ, ↑(u₁ / u₂) = (u₁ / u₂ : α) := by simp [div_eq_mul_inv]

Coercion of Unit Division Equals Division of Coercions

Informal description

For any units $u_1, u_2$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the canonical inclusion map $\alpha^\times \to \alpha$ satisfies $(u_1 / u_2) = u_1 / u_2$ in $\alpha$, where the left-hand side is the division in $\alpha^\times$ and the right-hand side is the division in $\alpha$.

Units.mkOfMulEqOne definition

[CommMonoid α] (a b : α) (hab : a * b = 1) : αˣ

Full source

/-- For `a, b` in a `CommMonoid` such that `a * b = 1`, makes a unit out of `a`. -/
@[to_additive
  "For `a, b` in an `AddCommMonoid` such that `a + b = 0`, makes an addUnit out of `a`."]
def Units.mkOfMulEqOne [CommMonoid α] (a b : α) (hab : a * b = 1) : αˣ :=
  ⟨a, b, hab, (mul_comm b a).trans hab⟩

Construction of a unit from elements with product one

Informal description

Given elements $a$ and $b$ in a commutative monoid $\alpha$ such that $a \cdot b = 1$, this constructs a unit (invertible element) of $\alpha$ from $a$ and $b$. The inverse of this unit is $b$.

Units.val_mkOfMulEqOne theorem

[CommMonoid α] {a b : α} (h : a * b = 1) : (Units.mkOfMulEqOne a b h : α) = a

Full source

@[to_additive (attr := simp)]
theorem Units.val_mkOfMulEqOne [CommMonoid α] {a b : α} (h : a * b = 1) :
    (Units.mkOfMulEqOne a b h : α) = a :=
  rfl

Underlying element of unit constructed from product-one pair equals first element

Informal description

Let $\alpha$ be a commutative monoid and let $a, b \in \alpha$ be elements such that $a \cdot b = 1$. Then the underlying element of the unit constructed from $a$ and $b$ via `Units.mkOfMulEqOne` equals $a$.

divp definition

(a : α) (u : Units α) : α

Full source

/-- Partial division, denoted `a /ₚ u`. It is defined when the
  second argument is invertible, and unlike the division operator
  in `DivisionRing` it is not totalized at zero. -/
def divp (a : α) (u : Units α) : α :=
  a * (u⁻¹ : αˣ)

Division by a unit in a monoid

Informal description

The operation $ a /ₚ u $ divides an element $ a $ of a monoid $ \alpha $ by a unit $ u $ of $ \alpha $, defined as $ a $ multiplied by the inverse of $ u $. This is a partial division operation that is only defined when the second argument is a unit (invertible element).

term_/ₚ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:70 " /ₚ " => divp

Division by a unit in a monoid

Informal description

The operation `a /ₚ u` divides an element `a` of a monoid `α` by a unit `u` of `α`. This is equivalent to multiplying `a` by the inverse of `u`.

divp_self theorem

(u : αˣ) : (u : α) /ₚ u = 1

Full source

@[simp]
theorem divp_self (u : αˣ) : (u : α) /ₚ u = 1 :=
  Units.mul_inv _

Division of Unit by Itself Yields Identity

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, dividing $u$ (considered as an element of $\alpha$) by itself yields the multiplicative identity, i.e., $u /ₚ u = 1$.

divp_one theorem

(a : α) : a /ₚ 1 = a

Full source

@[simp]
theorem divp_one (a : α) : a /ₚ 1 = a :=
  mul_one _

Division by Identity Unit Yields Original Element

Informal description

For any element $a$ in a monoid $\alpha$, dividing $a$ by the unit $1$ (the multiplicative identity) yields $a$ itself, i.e., $a /ₚ 1 = a$.

divp_assoc theorem

(a b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u)

Full source

theorem divp_assoc (a b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u) :=
  mul_assoc _ _ _

Associativity of Division by a Unit in a Monoid

Informal description

For any elements $a, b$ in a monoid $\alpha$ and any unit $u \in \alpha^\times$, the operation of dividing the product $a \cdot b$ by $u$ is equal to $a$ multiplied by the division of $b$ by $u$, i.e., $(a \cdot b) /ₚ u = a \cdot (b /ₚ u)$.

divp_assoc' theorem

(x y : α) (u : αˣ) : x * (y /ₚ u) = x * y /ₚ u

Full source

/-- `field_simp` needs the reverse direction of `divp_assoc` to move all `/ₚ` to the right. -/
@[field_simps]
theorem divp_assoc' (x y : α) (u : αˣ) : x * (y /ₚ u) = x * y /ₚ u :=
  (divp_assoc _ _ _).symm

Associativity of Division by Unit: $x \cdot (y /ₚ u) = (x \cdot y) /ₚ u$

Informal description

For any elements $x, y$ in a monoid $\alpha$ and any unit $u \in \alpha^\times$, the product $x \cdot (y /ₚ u)$ is equal to $(x \cdot y) /ₚ u$, where $/ₚ$ denotes division by a unit.

divp_inv theorem

(u : αˣ) : a /ₚ u⁻¹ = a * u

Full source

@[simp]
theorem divp_inv (u : αˣ) : a /ₚ u⁻¹ = a * u :=
  rfl

Division by Inverse Unit Equals Multiplication by Unit: $a /ₚ u^{-1} = a \cdot u$

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, and for any element $a \in \alpha$, the division $a /ₚ u^{-1}$ is equal to the product $a \cdot u$.

divp_mul_cancel theorem

(a : α) (u : αˣ) : a /ₚ u * u = a

Full source

@[simp]
theorem divp_mul_cancel (a : α) (u : αˣ) : a /ₚ u * u = a :=
  (mul_assoc _ _ _).trans <| by rw [Units.inv_mul, mul_one]

Division by Unit Cancellation: $(a /ₚ u) \cdot u = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u \in \alpha^\times$, the operation $(a /ₚ u) \cdot u$ equals $a$, where $/ₚ$ denotes division by a unit.

mul_divp_cancel theorem

(a : α) (u : αˣ) : a * u /ₚ u = a

Full source

@[simp]
theorem mul_divp_cancel (a : α) (u : αˣ) : a * u /ₚ u = a :=
  (mul_assoc _ _ _).trans <| by rw [Units.mul_inv, mul_one]

Cancellation of Multiplication by a Unit: $(a \cdot u) /\!_p u = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ in $\alpha^\times$, the operation $(a \cdot u) /\!_p u$ equals $a$, where $/\!_p$ denotes division by a unit.

divp_divp_eq_divp_mul theorem

(x : α) (u₁ u₂ : αˣ) : x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

Full source

@[field_simps]
theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) : x /ₚ u₁x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁) := by
  simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]

Double Division by Units Equals Division by Product: $(x /ₚ u_1) /ₚ u_2 = x /ₚ (u_2 \cdot u_1)$

Informal description

For any element $x$ in a monoid $\alpha$ and any units $u_1, u_2 \in \alpha^\times$, the operation of dividing $x$ by $u_1$ and then by $u_2$ is equivalent to dividing $x$ by the product $u_2 \cdot u_1$. That is, $(x /ₚ u_1) /ₚ u_2 = x /ₚ (u_2 \cdot u_1)$.

one_divp theorem

(u : αˣ) : 1 /ₚ u = ↑u⁻¹

Full source

@[simp]
theorem one_divp (u : αˣ) : 1 /ₚ u = ↑u⁻¹ :=
  one_mul _

Division of One by a Unit Equals its Inverse: $1 /ₚ u = u^{-1}$

Informal description

For any unit $u$ in a monoid $\alpha$, the division of the multiplicative identity $1$ by $u$ equals the inverse of $u$, i.e., $1 /ₚ u = u^{-1}$.

inv_eq_one_divp theorem

(u : αˣ) : ↑u⁻¹ = 1 /ₚ u

Full source

/-- Used for `field_simp` to deal with inverses of units. -/
@[field_simps]
theorem inv_eq_one_divp (u : αˣ) : ↑u⁻¹ = 1 /ₚ u := by rw [one_divp]

Inverse as Division of One by Unit: $u^{-1} = 1 /ₚ u$

Informal description

For any unit $u$ in a monoid $\alpha$, the inverse of $u$ is equal to the division of $1$ by $u$, i.e., $u^{-1} = 1 /ₚ u$.

val_div_eq_divp theorem

(u₁ u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Full source

/-- `field_simp` moves division inside `αˣ` to the right, and this lemma
lifts the calculation to `α`.
-/
@[field_simps]
theorem val_div_eq_divp (u₁ u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ /ₚ u₂ := by
  rw [divp, division_def, Units.val_mul]

Canonical Map Preserves Division of Units: $\overline{u_1 / u_2} = \overline{u_1} /ₚ u_2$

Informal description

For any units $u_1$ and $u_2$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the canonical map from $\alpha^\times$ to $\alpha$ satisfies $\overline{(u_1 / u_2)} = \overline{u_1} /ₚ u_2$, where $\overline{u}$ denotes the image of $u$ under the canonical map and $/ₚ$ denotes division by a unit in $\alpha$.

IsUnit definition

[Monoid M] (a : M) : Prop

Full source

/-- An element `a : M` of a `Monoid` is a unit if it has a two-sided inverse.
The actual definition says that `a` is equal to some `u : Mˣ`, where
`Mˣ` is a bundled version of `IsUnit`. -/
@[to_additive "An element `a : M` of an `AddMonoid` is an `AddUnit` if it has a two-sided additive
inverse. The actual definition says that `a` is equal to some `u : AddUnits M`,
where `AddUnits M` is a bundled version of `IsAddUnit`."]
def IsUnit [Monoid M] (a : M) : Prop :=
  ∃ u : Mˣ, (u : M) = a

Predicate for being a unit in a monoid

Informal description

A predicate asserting that an element $ a $ of a monoid $ M $ is a unit, meaning there exists an invertible element $ u $ in the group of units $ M^\times $ such that $ u = a $. Equivalently, $ a $ is a unit if there exists an element $ b $ in $ M $ such that $ a \cdot b = 1 $ and $ b \cdot a = 1 $.

isUnit_iff_exists theorem

[Monoid M] {x : M} : IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1

Full source

/-- See `isUnit_iff_exists_and_exists` for a similar lemma with two existentials. -/
@[to_additive "See `isAddUnit_iff_exists_and_exists` for a similar lemma with two existentials."]
lemma isUnit_iff_exists [Monoid M] {x : M} : IsUnitIsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1 := by
  refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩
  subst x
  exact ⟨u.inv, u.val_inv, u.inv_val⟩

Characterization of Units via Two-Sided Inverses

Informal description

An element $x$ of a monoid $M$ is a unit if and only if there exists an element $b \in M$ such that $x \cdot b = 1$ and $b \cdot x = 1$.

isUnit_iff_exists_and_exists theorem

[Monoid M] {a : M} : IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1)

Full source

/-- See `isUnit_iff_exists` for a similar lemma with one existential. -/
@[to_additive "See `isAddUnit_iff_exists` for a similar lemma with one existential."]
theorem isUnit_iff_exists_and_exists [Monoid M] {a : M} :
    IsUnitIsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1) :=
  isUnit_iff_exists.trans
    ⟨fun ⟨b, hba, hab⟩ => ⟨⟨b, hba⟩, ⟨b, hab⟩⟩,
      fun ⟨⟨b, hb⟩, ⟨_, hc⟩⟩ => ⟨b, hb, left_inv_eq_right_inv hc hb ▸ hc⟩⟩

Characterization of Units via Left and Right Inverses

Informal description

An element $a$ of a monoid $M$ is a unit if and only if there exists an element $b \in M$ such that $a \cdot b = 1$ and there exists an element $c \in M$ such that $c \cdot a = 1$.

Units.isUnit theorem

[Monoid M] (u : Mˣ) : IsUnit (u : M)

Full source

@[to_additive (attr := simp)]
protected theorem Units.isUnit [Monoid M] (u : Mˣ) : IsUnit (u : M) :=
  ⟨u, rfl⟩

Units are invertible elements

Informal description

For any monoid $M$ and any element $u$ in the group of units $M^\times$, the element $u$ is a unit in $M$ (i.e., $u$ is invertible).

isUnit_one theorem

[Monoid M] : IsUnit (1 : M)

Full source

@[to_additive (attr := simp)]
theorem isUnit_one [Monoid M] : IsUnit (1 : M) :=
  ⟨1, rfl⟩

Identity Element is a Unit in a Monoid

Informal description

In any monoid $M$, the multiplicative identity element $1$ is a unit (i.e., invertible).

isUnit_of_mul_eq_one theorem

[CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit a

Full source

@[to_additive]
theorem isUnit_of_mul_eq_one [CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit a :=
  ⟨Units.mkOfMulEqOne a b h, rfl⟩

Product with Identity Implies Invertibility in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any elements $a, b \in M$ such that $a \cdot b = 1$, the element $a$ is a unit (i.e., invertible) in $M$.

isUnit_of_mul_eq_one_right theorem

[CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit b

Full source

@[to_additive]
theorem isUnit_of_mul_eq_one_right [CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit b := by
  rw [mul_comm] at h
  exact isUnit_of_mul_eq_one b a h

Right Factor Invertibility in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any elements $a, b \in M$ such that $a \cdot b = 1$, the element $b$ is a unit (i.e., invertible) in $M$.

IsUnit.exists_right_inv theorem

(h : IsUnit a) : ∃ b, a * b = 1

Full source

@[to_additive IsAddUnit.exists_neg]
lemma IsUnit.exists_right_inv (h : IsUnit a) : ∃ b, a * b = 1 := by
  rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
  exact ⟨b, hab⟩

Existence of Right Inverse for Units in a Monoid

Informal description

For any element $a$ in a monoid $M$, if $a$ is a unit (i.e., invertible), then there exists an element $b \in M$ such that $a \cdot b = 1$.

IsUnit.exists_left_inv theorem

{a : M} (h : IsUnit a) : ∃ b, b * a = 1

Full source

@[to_additive IsAddUnit.exists_neg']
lemma IsUnit.exists_left_inv {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by
  rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
  exact ⟨b, hba⟩

Existence of Left Inverse for Units in a Monoid

Informal description

For any element $a$ in a monoid $M$, if $a$ is a unit (i.e., invertible), then there exists an element $b \in M$ such that $b \cdot a = 1$.

IsUnit.mul theorem

: IsUnit a → IsUnit b → IsUnit (a * b)

Full source

@[to_additive] lemma IsUnit.mul : IsUnit a → IsUnit b → IsUnit (a * b) := by
  rintro ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x * y, rfl⟩

Product of Units is a Unit

Informal description

For any elements $a$ and $b$ in a monoid $M$, if $a$ is a unit and $b$ is a unit, then their product $a \cdot b$ is also a unit.

IsUnit.pow theorem

(n : ℕ) : IsUnit a → IsUnit (a ^ n)

Full source

@[to_additive] lemma IsUnit.pow (n : ℕ) : IsUnit a → IsUnit (a ^ n) := by
  rintro ⟨u, rfl⟩; exact ⟨u ^ n, rfl⟩

Powers of Units are Units

Informal description

For any natural number $n$ and any element $a$ in a monoid $M$, if $a$ is a unit, then $a^n$ is also a unit.

isUnit_iff_eq_one theorem

[Subsingleton Mˣ] {x : M} : IsUnit x ↔ x = 1

Full source

@[to_additive (attr := simp)]
lemma isUnit_iff_eq_one [Subsingleton Mˣ] {x : M} : IsUnitIsUnit x ↔ x = 1 :=
  ⟨fun ⟨u, hu⟩ ↦ by rw [← hu, Subsingleton.elim u 1, Units.val_one], fun h ↦ h ▸ isUnit_one⟩

Characterization of Units in Monoids with Unique Unit

Informal description

Let $M$ be a monoid such that its group of units $M^\times$ is a subsingleton (i.e., has at most one element). Then for any element $x \in M$, $x$ is a unit if and only if $x$ is equal to the identity element $1$.

isUnit_iff_exists_inv theorem

[CommMonoid M] {a : M} : IsUnit a ↔ ∃ b, a * b = 1

Full source

@[to_additive]
theorem isUnit_iff_exists_inv [CommMonoid M] {a : M} : IsUnitIsUnit a ↔ ∃ b, a * b = 1 :=
  ⟨fun h => h.exists_right_inv, fun ⟨b, hab⟩ => isUnit_of_mul_eq_one _ b hab⟩

Characterization of Units in Commutative Monoids via Right Inverses

Informal description

Let $M$ be a commutative monoid. An element $a \in M$ is a unit if and only if there exists an element $b \in M$ such that $a \cdot b = 1$.

isUnit_iff_exists_inv' theorem

[CommMonoid M] {a : M} : IsUnit a ↔ ∃ b, b * a = 1

Full source

@[to_additive]
theorem isUnit_iff_exists_inv' [CommMonoid M] {a : M} : IsUnitIsUnit a ↔ ∃ b, b * a = 1 := by
  simp [isUnit_iff_exists_inv, mul_comm]

Characterization of Units in Commutative Monoids via Left Inverses

Informal description

Let $M$ be a commutative monoid. An element $a \in M$ is a unit if and only if there exists an element $b \in M$ such that $b \cdot a = 1$.

Units.isUnit_mul_units theorem

[Monoid M] (a : M) (u : Mˣ) : IsUnit (a * u) ↔ IsUnit a

Full source

/-- Multiplication by a `u : Mˣ` on the right doesn't affect `IsUnit`. -/
@[to_additive (attr := simp)
"Addition of a `u : AddUnits M` on the right doesn't affect `IsAddUnit`."]
theorem Units.isUnit_mul_units [Monoid M] (a : M) (u : Mˣ) : IsUnitIsUnit (a * u) ↔ IsUnit a :=
  Iff.intro
    (fun ⟨v, hv⟩ => by
      have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
      rwa [mul_assoc, Units.mul_inv, mul_one] at this)
    fun v => v.mul u.isUnit

Product with Unit is Unit iff Original Element is Unit

Informal description

Let $M$ be a monoid. For any element $a \in M$ and any unit $u \in M^\times$, the product $a \cdot u$ is a unit if and only if $a$ itself is a unit.

Units.isUnit_units_mul theorem

{M : Type*} [Monoid M] (u : Mˣ) (a : M) : IsUnit (↑u * a) ↔ IsUnit a

Full source

/-- Multiplication by a `u : Mˣ` on the left doesn't affect `IsUnit`. -/
@[to_additive (attr := simp)
"Addition of a `u : AddUnits M` on the left doesn't affect `IsAddUnit`."]
theorem Units.isUnit_units_mul {M : Type*} [Monoid M] (u : Mˣ) (a : M) :
    IsUnitIsUnit (↑u * a) ↔ IsUnit a :=
  Iff.intro
    (fun ⟨v, hv⟩ => by
      have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
      rwa [← mul_assoc, Units.inv_mul, one_mul] at this)
    u.isUnit.mul

Multiplication by a unit preserves invertibility: $u \cdot a$ is invertible iff $a$ is invertible

Informal description

Let $M$ be a monoid, $u$ be a unit in $M$ (i.e., $u \in M^\times$), and $a$ be an element of $M$. Then the product $u \cdot a$ is a unit if and only if $a$ is a unit.

isUnit_of_mul_isUnit_left theorem

[CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit x

Full source

@[to_additive]
theorem isUnit_of_mul_isUnit_left [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit x :=
  let ⟨z, hz⟩ := isUnit_iff_exists_inv.1 hu
  isUnit_iff_exists_inv.2 ⟨y * z, by rwa [← mul_assoc]⟩

Left Factor is Unit When Product is Unit in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any elements $x, y \in M$, if the product $x \cdot y$ is a unit, then $x$ is a unit.

isUnit_of_mul_isUnit_right theorem

[CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit y

Full source

@[to_additive]
theorem isUnit_of_mul_isUnit_right [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit y :=
  @isUnit_of_mul_isUnit_left _ _ y x <| by rwa [mul_comm]

Right Factor is Unit When Product is Unit in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any elements $x, y \in M$, if the product $x \cdot y$ is a unit, then $y$ is a unit.

IsUnit.mul_iff theorem

[CommMonoid M] {x y : M} : IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y

Full source

@[to_additive (attr := simp)]
theorem mul_iff [CommMonoid M] {x y : M} : IsUnitIsUnit (x * y) ↔ IsUnit x ∧ IsUnit y :=
  ⟨fun h => ⟨isUnit_of_mul_isUnit_left h, isUnit_of_mul_isUnit_right h⟩,
   fun h => IsUnit.mul h.1 h.2⟩

Product is Unit iff Both Factors Are Units in Commutative Monoid

Informal description

Let $M$ be a commutative monoid. For any elements $x, y \in M$, the product $x \cdot y$ is a unit if and only if both $x$ and $y$ are units.

IsUnit.unit definition

(h : IsUnit a) : Mˣ

Full source

/-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
`α` is a `DivisionMonoid`, use `IsUnit.unit'` instead. -/
@[to_additive "The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. When `α` is a `SubtractionMonoid`, use
`IsAddUnit.addUnit'` instead."]
protected noncomputable def unit (h : IsUnit a) : Mˣ :=
  (Classical.choose h).copy a (Classical.choose_spec h).symm _ rfl

Unit element corresponding to a provably invertible element

Informal description

Given a proof `h` that an element `a` of a monoid `M` is a unit, this function returns the corresponding unit element in the group of units `Mˣ`, ensuring that the underlying value of this unit is equal to `a`.

IsUnit.unit_of_val_units theorem

{a : Mˣ} (h : IsUnit (a : M)) : h.unit = a

Full source

@[to_additive (attr := simp)]
theorem unit_of_val_units {a : Mˣ} (h : IsUnit (a : M)) : h.unit = a :=
  Units.ext <| rfl

Equality of Constructed Unit with Original Unit

Informal description

For any unit $a$ in the group of units $M^\times$ of a monoid $M$, if $a$ is provably invertible as an element of $M$ (i.e., $\text{IsUnit}(a)$ holds), then the unit element constructed from this proof is equal to $a$ itself.

IsUnit.unit_spec theorem

(h : IsUnit a) : ↑h.unit = a

Full source

@[to_additive (attr := simp)]
theorem unit_spec (h : IsUnit a) : ↑h.unit = a :=
  rfl

Underlying Value of Unit Element Equals Original Element

Informal description

For any element $a$ of a monoid $M$ that is a unit (i.e., invertible), the underlying value of the corresponding unit element $h.\text{unit}$ is equal to $a$, i.e., $h.\text{unit} = a$.

IsUnit.unit_one theorem

(h : IsUnit (1 : M)) : h.unit = 1

Full source

@[to_additive (attr := simp)]
theorem unit_one (h : IsUnit (1 : M)) : h.unit = 1 :=
  Units.eq_iff.1 rfl

Unit of One is Identity in Group of Units

Informal description

For any monoid $M$, if $1$ is a unit (which it always is), then the corresponding unit element in the group of units $M^\times$ is the identity element $1$.

IsUnit.val_inv_mul theorem

(h : IsUnit a) : ↑h.unit⁻¹ * a = 1

Full source

@[to_additive (attr := simp)]
theorem val_inv_mul (h : IsUnit a) : ↑h.unit⁻¹ * a = 1 :=
  Units.mul_inv _

Inverse of Unit Multiplied by Element Yields Identity

Informal description

For any element $a$ in a monoid $M$ that is a unit (i.e., invertible), the product of the inverse of the corresponding unit element and $a$ equals the multiplicative identity, i.e., $u^{-1} \cdot a = 1$, where $u$ is the unit associated with $a$.

IsUnit.mul_val_inv theorem

(h : IsUnit a) : a * ↑h.unit⁻¹ = 1

Full source

@[to_additive (attr := simp)]
theorem mul_val_inv (h : IsUnit a) : a * ↑h.unit⁻¹ = 1 := by
  rw [← h.unit.mul_inv]; congr

Multiplication of a Unit by its Inverse Yields Identity

Informal description

For any element $a$ in a monoid $M$, if $a$ is a unit (i.e., invertible), then $a$ multiplied by the inverse of its corresponding unit element equals the multiplicative identity, i.e., $a \cdot (h.\text{unit})^{-1} = 1$.

IsUnit.instDecidableOfExistsUnitsEqVal instance

(x : M) [h : Decidable (∃ u : Mˣ, ↑u = x)] : Decidable (IsUnit x)

Full source

/-- `IsUnit x` is decidable if we can decide if `x` comes from `Mˣ`. -/
@[to_additive "`IsAddUnit x` is decidable if we can decide if `x` comes from `AddUnits M`."]
instance (x : M) [h : Decidable (∃ u : Mˣ, ↑u = x)] : Decidable (IsUnit x) :=
  h

Decidability of the IsUnit Predicate via Units

Informal description

For any element $x$ in a monoid $M$, the predicate `IsUnit x` (asserting that $x$ is invertible) is decidable if we can decide whether there exists a unit $u \in M^\times$ such that $u = x$.

IsUnit.inv_mul_cancel theorem

: IsUnit a → a⁻¹ * a = 1

Full source

@[to_additive (attr := simp)]
protected theorem inv_mul_cancel : IsUnit a → a⁻¹ * a = 1 := by
  rintro ⟨u, rfl⟩
  rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

Left inverse property for units: $a^{-1} \cdot a = 1$

Informal description

For any element $a$ in a monoid $M$, if $a$ is a unit (i.e., invertible), then the product of its inverse and itself equals the multiplicative identity, i.e., $a^{-1} \cdot a = 1$.

IsUnit.mul_inv_cancel theorem

: IsUnit a → a * a⁻¹ = 1

Full source

@[to_additive (attr := simp)]
protected theorem mul_inv_cancel : IsUnit a → a * a⁻¹ = 1 := by
  rintro ⟨u, rfl⟩
  rw [← Units.val_inv_eq_inv_val, Units.mul_inv]

Multiplication of a Unit by its Inverse Yields Identity

Informal description

If an element $a$ of a monoid $M$ is a unit (i.e., invertible), then $a$ multiplied by its inverse equals the identity element, i.e., $a \cdot a^{-1} = 1$.

IsUnit.unit' definition

(h : IsUnit a) : αˣ

Full source

/-- The element of the group of units, corresponding to an element of a monoid which is a unit. As
opposed to `IsUnit.unit`, the inverse is computable and comes from the inversion on `α`. This is
useful to transfer properties of inversion in `Units α` to `α`. See also `toUnits`. -/
@[to_additive (attr := simps val)
"The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. As opposed to `IsAddUnit.addUnit`, the negation is
computable and comes from the negation on `α`. This is useful to transfer properties of negation
in `AddUnits α` to `α`. See also `toAddUnits`."]
def unit' (h : IsUnit a) : αˣ := ⟨a, a⁻¹, h.mul_inv_cancel, h.inv_mul_cancel⟩

Construction of a unit element from a proof of invertibility

Informal description

Given an element $ a $ of a monoid $ \alpha $ and a proof $ h $ that $ a $ is a unit, the function `IsUnit.unit'` constructs an element of the group of units $ \alpha^\times $ consisting of $ a $ paired with its inverse $ a^{-1} $, satisfying the properties $ a \cdot a^{-1} = 1 $ and $ a^{-1} \cdot a = 1 $.

IsUnit.val_inv_unit' theorem

(h : IsUnit a) : ↑(h.unit'⁻¹) = a⁻¹

Full source

@[to_additive] lemma val_inv_unit' (h : IsUnit a) : ↑(h.unit'⁻¹) = a⁻¹ := rfl

Inverse of Constructed Unit Element Equals Element's Inverse

Informal description

For any element $a$ in a monoid $\alpha$ that is a unit (i.e., invertible), the inverse of the constructed unit element $h.\text{unit}'$ (when coerced back to $\alpha$) equals the inverse of $a$, i.e., $(h.\text{unit}')^{-1} = a^{-1}$.

IsUnit.mul_inv_cancel_left theorem

(h : IsUnit a) : ∀ b, a * (a⁻¹ * b) = b

Full source

@[to_additive (attr := simp)]
protected lemma mul_inv_cancel_left (h : IsUnit a) : ∀ b, a * (a⁻¹ * b) = b :=
  h.unit'.mul_inv_cancel_left

Left Cancellation Property for Invertible Elements: $a \cdot (a^{-1} \cdot b) = b$

Informal description

For any element $a$ in a monoid $M$ that is a unit (i.e., invertible), and for any element $b \in M$, the following holds: \[ a \cdot (a^{-1} \cdot b) = b. \]

IsUnit.inv_mul_cancel_left theorem

(h : IsUnit a) : ∀ b, a⁻¹ * (a * b) = b

Full source

@[to_additive (attr := simp)]
protected lemma inv_mul_cancel_left (h : IsUnit a) : ∀ b, a⁻¹ * (a * b) = b :=
  h.unit'.inv_mul_cancel_left

Left cancellation property for invertible elements: $a^{-1} \cdot (a \cdot b) = b$

Informal description

For any element $a$ in a monoid $M$ that is a unit (i.e., invertible), and for any element $b \in M$, the following identity holds: $a^{-1} \cdot (a \cdot b) = b$.

IsUnit.div_self theorem

(h : IsUnit a) : a / a = 1

Full source

@[to_additive]
protected lemma div_self (h : IsUnit a) : a / a = 1 := by rw [div_eq_mul_inv, h.mul_inv_cancel]

Division of a Unit by Itself Yields Identity

Informal description

For any unit element $a$ in a monoid $M$, the division of $a$ by itself yields the identity element, i.e., $a / a = 1$.

IsUnit.inv theorem

(h : IsUnit a) : IsUnit a⁻¹

Full source

@[to_additive]
lemma inv (h : IsUnit a) : IsUnit a⁻¹ := by
  obtain ⟨u, hu⟩ := h
  rw [← hu, ← Units.val_inv_eq_inv_val]
  exact Units.isUnit _

Inverse of a Unit is a Unit

Informal description

If an element $a$ of a monoid $M$ is a unit (i.e., invertible), then its inverse $a^{-1}$ is also a unit.

IsUnit.div theorem

(ha : IsUnit a) (hb : IsUnit b) : IsUnit (a / b)

Full source

@[to_additive] lemma div (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a / b) := by
  rw [div_eq_mul_inv]; exact ha.mul hb.inv

Quotient of Units is a Unit

Informal description

For any elements $a$ and $b$ in a monoid $M$, if $a$ is a unit and $b$ is a unit, then their quotient $a / b$ is also a unit.

IsUnit.div_mul_cancel_right theorem

(h : IsUnit b) (a : α) : b / (a * b) = a⁻¹

Full source

@[to_additive]
protected lemma div_mul_cancel_right (h : IsUnit b) (a : α) : b / (a * b) = a⁻¹ := by
  rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

Right Cancellation Property for Units: $b / (a \cdot b) = a^{-1}$

Informal description

For any element $b$ in a monoid $\alpha$ that is a unit (i.e., invertible), and for any element $a \in \alpha$, the following holds: \[ b / (a \cdot b) = a^{-1}. \]

IsUnit.mul_div_mul_right theorem

(h : IsUnit c) (a b : α) : a * c / (b * c) = a / b

Full source

@[to_additive]
protected lemma mul_div_mul_right (h : IsUnit c) (a b : α) : a * c / (b * c) = a / b := by
  simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

Right Cancellation Property for Units: $(a \cdot c) / (b \cdot c) = a / b$

Informal description

For any elements $a, b, c$ in a monoid $\alpha$, if $c$ is a unit, then the following equality holds: \[ (a \cdot c) / (b \cdot c) = a / b. \]

IsUnit.div_mul_cancel_left theorem

(h : IsUnit a) (b : α) : a / (a * b) = b⁻¹

Full source

@[to_additive]
protected lemma div_mul_cancel_left (h : IsUnit a) (b : α) : a / (a * b) = b⁻¹ := by
  rw [mul_comm, h.div_mul_cancel_right]

Left Cancellation Property for Units: $a / (a \cdot b) = b^{-1}$

Informal description

For any element $a$ in a monoid $\alpha$ that is a unit (i.e., invertible), and for any element $b \in \alpha$, the following holds: \[ a / (a \cdot b) = b^{-1}. \]

IsUnit.mul_div_mul_left theorem

(h : IsUnit c) (a b : α) : c * a / (c * b) = a / b

Full source

@[to_additive]
protected lemma mul_div_mul_left (h : IsUnit c) (a b : α) : c * a / (c * b) = a / b := by
  rw [mul_comm c, mul_comm c, h.mul_div_mul_right]

Left Cancellation Property for Units: $(c \cdot a) / (c \cdot b) = a / b$

Informal description

For any elements $a, b, c$ in a monoid $\alpha$, if $c$ is a unit, then the following equality holds: \[ (c \cdot a) / (c \cdot b) = a / b. \]

divp_eq_div theorem

[DivisionMonoid α] (a : α) (u : αˣ) : a /ₚ u = a / u

Full source

@[field_simps]
lemma divp_eq_div [DivisionMonoid α] (a : α) (u : αˣ) : a /ₚ u = a / u := by
  rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]

Equality of Division Operations in a Division Monoid: $a /ₚ u = a / u$

Informal description

In a division monoid $\alpha$, for any element $a \in \alpha$ and any unit $u \in \alpha^\times$, the division operation $a /ₚ u$ (division by a unit) is equal to the standard division operation $a / u$.

Group.isUnit theorem

[Group α] (a : α) : IsUnit a

Full source

@[to_additive]
lemma Group.isUnit [Group α] (a : α) : IsUnit a :=
  ⟨⟨a, a⁻¹, mul_inv_cancel _, inv_mul_cancel _⟩, rfl⟩

Every Element in a Group is a Unit

Informal description

For any element $a$ in a group $\alpha$, $a$ is a unit (i.e., invertible).

invOfIsUnit definition

[Monoid M] (h : ∀ a : M, IsUnit a) : Inv M

Full source

/-- Constructs an inv operation for a `Monoid` consisting only of units. -/
noncomputable def invOfIsUnit [Monoid M] (h : ∀ a : M, IsUnit a) : Inv M where
  inv := fun a => ↑(h a).unit⁻¹

Inversion operation for a monoid where all elements are units

Informal description

Given a monoid $ M $ where every element is invertible (i.e., for every $ a \in M $, there exists $ b \in M $ such that $ a \cdot b = 1 $ and $ b \cdot a = 1 $), this constructs an inversion operation on $ M $. The inversion of an element $ a $ is defined as the inverse of the corresponding unit in the group of units $ M^\times $.

groupOfIsUnit definition

[hM : Monoid M] (h : ∀ a : M, IsUnit a) : Group M

Full source

/-- Constructs a `Group` structure on a `Monoid` consisting only of units. -/
noncomputable def groupOfIsUnit [hM : Monoid M] (h : ∀ a : M, IsUnit a) : Group M :=
  { hM with
    toInv := invOfIsUnit h,
    inv_mul_cancel := fun a => by
      change ↑(h a).unit⁻¹ * a = 1
      rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one] }

Group structure on a monoid of units

Informal description

Given a monoid $ M $ where every element is invertible (i.e., for every $ a \in M $, the predicate $\text{IsUnit } a$ holds), this constructs a group structure on $ M $. The inversion operation is defined via the existing units, and satisfies the group axioms.

commGroupOfIsUnit definition

[hM : CommMonoid M] (h : ∀ a : M, IsUnit a) : CommGroup M

Full source

/-- Constructs a `CommGroup` structure on a `CommMonoid` consisting only of units. -/
noncomputable def commGroupOfIsUnit [hM : CommMonoid M] (h : ∀ a : M, IsUnit a) : CommGroup M :=
  { hM with
    toInv := invOfIsUnit h,
    inv_mul_cancel := fun a => by
      change ↑(h a).unit⁻¹ * a = 1
      rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one] }

Commutative group structure on a monoid of units

Informal description

Given a commutative monoid $ M $ where every element is a unit (i.e., invertible), this constructs a commutative group structure on $ M $. The inversion operation is defined via `invOfIsUnit`, and the group axioms are satisfied by the properties of units in $ M $.

Mathlib.Algebra.Group.Units.Defs

Main declarations

Notation

TODO