Mathlib.Algebra.Group.Units.Basic

unique_one theorem

{α : Type*} [Unique α] [One α] : default = (1 : α)

Full source

@[to_additive]
theorem unique_one {α : Type*} [Unique α] [One α] : default = (1 : α) :=
  Unique.default_eq 1

Default Element Equals One in Unique Monoids

Informal description

In a type $\alpha$ with exactly one element and equipped with a multiplicative identity $1$, the default element of $\alpha$ is equal to $1$.

Units.mul_inv_cancel_right theorem

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

Full source

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

Right multiplication by a unit and its inverse preserves the original element

Informal description

For any element $a$ in a monoid $\alpha$ and any invertible element $b$ in the units of $\alpha$, the product $a \cdot b \cdot b^{-1}$ equals $a$.

Units.inv_mul_cancel_right theorem

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

Full source

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

Right cancellation property for invertible elements: $a * b^{-1} * b = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any invertible element $b$ in $\alpha$, the operation $a * b^{-1} * b$ simplifies to $a$.

Units.mul_right_inj theorem

(a : αˣ) {b c : α} : (a : α) * b = a * c ↔ b = c

Full source

@[to_additive (attr := simp)]
theorem mul_right_inj (a : αˣ) {b c : α} : (a : α) * b = a * c ↔ b = c :=
  ⟨fun h => by simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h,
    congr_arg _⟩

Right Cancellation Property for Multiplication by a Unit

Informal description

Let $a$ be a unit (invertible element) in a monoid $\alpha$, and let $b, c$ be elements of $\alpha$. Then $a \cdot b = a \cdot c$ if and only if $b = c$.

Units.mul_left_inj theorem

(a : αˣ) {b c : α} : b * a = c * a ↔ b = c

Full source

@[to_additive (attr := simp)]
theorem mul_left_inj (a : αˣ) {b c : α} : b * a = c * a ↔ b = c :=
  ⟨fun h => by simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h,
    congr_arg (· * a.val)⟩

Left Cancellation Property for Multiplication by a Unit

Informal description

Let $a$ be a unit (invertible element) in a monoid $\alpha$, and let $b, c$ be elements of $\alpha$. Then $b \cdot a = c \cdot a$ if and only if $b = c$.

Units.mul_inv_eq_iff_eq_mul theorem

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

Full source

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

Equivalence of right multiplication by inverse and original multiplication: $a \cdot b^{-1} = c \leftrightarrow a = c \cdot b$

Informal description

For any elements $a$ and $c$ in a monoid $\alpha$ and any invertible element $b$ in $\alpha$, the equation $a \cdot b^{-1} = c$ holds if and only if $a = c \cdot b$.

Units.inv_eq_of_mul_eq_one_left theorem

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

Full source

@[to_additive]
protected theorem inv_eq_of_mul_eq_one_left {a : α} (h : a * u = 1) : ↑u⁻¹ = a :=
  calc
    ↑u⁻¹ = 1 * ↑u⁻¹ := by rw [one_mul]
    _ = a := by rw [← h, mul_inv_cancel_right]

Inverse characterization via left multiplication identity

Informal description

Let $u$ be a unit (invertible element) in a monoid $\alpha$ and let $a \in \alpha$. If $a \cdot u = 1$, then the inverse of $u$ equals $a$, i.e., $u^{-1} = a$.

Units.inv_eq_of_mul_eq_one_right theorem

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

Full source

@[to_additive]
protected theorem inv_eq_of_mul_eq_one_right {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
  calc
    ↑u⁻¹ = ↑u⁻¹ * 1 := by rw [mul_one]
    _ = a := by rw [← h, inv_mul_cancel_left]

Inverse characterization via right multiplication identity

Informal description

Let $u$ be a unit (invertible element) in a monoid $\alpha$ and let $a \in \alpha$. If $u \cdot a = 1$, then the inverse of $u$ equals $a$, i.e., $u^{-1} = a$.

Units.mul_inv_eq_one theorem

{a : α} : a * ↑u⁻¹ = 1 ↔ a = u

Full source

@[to_additive (attr := simp)]
theorem mul_inv_eq_one {a : α} : a * ↑u⁻¹ = 1 ↔ a = u :=
  ⟨inv_inv u ▸ Units.eq_inv_of_mul_eq_one_right, fun h => mul_inv_of_eq h.symm⟩

Unit Condition: $a \cdot u^{-1} = 1 \leftrightarrow a = u$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ in $\alpha$, the product $a \cdot u^{-1}$ equals the identity element $1$ if and only if $a = u$.

Units.inv_mul_eq_one theorem

{a : α} : ↑u⁻¹ * a = 1 ↔ ↑u = a

Full source

@[to_additive (attr := simp)]
theorem inv_mul_eq_one {a : α} : ↑u⁻¹ * a = 1 ↔ ↑u = a :=
  ⟨inv_inv u ▸ Units.inv_eq_of_mul_eq_one_right, inv_mul_of_eq⟩

Unit Condition: $u^{-1} \cdot a = 1 \leftrightarrow u = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ in $\alpha$, the product $u^{-1} \cdot a$ equals the identity element $1$ if and only if $u = a$.

Units.mul_eq_one_iff_eq_inv theorem

{a : α} : a * u = 1 ↔ a = ↑u⁻¹

Full source

@[to_additive]
theorem mul_eq_one_iff_eq_inv {a : α} : a * u = 1 ↔ a = ↑u⁻¹ := by rw [← mul_inv_eq_one, inv_inv]

Unit Condition: $a \cdot u = 1 \leftrightarrow a = u^{-1}$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ in $\alpha$, the product $a \cdot u$ equals the identity element $1$ if and only if $a$ is equal to the inverse of $u$.

Units.mul_eq_one_iff_inv_eq theorem

{a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a

Full source

@[to_additive]
theorem mul_eq_one_iff_inv_eq {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a := by rw [← inv_mul_eq_one, inv_inv]

Unit Condition: $u \cdot a = 1 \leftrightarrow u^{-1} = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ in $\alpha$, the product $u \cdot a$ equals the identity element $1$ if and only if the inverse of $u$ equals $a$, i.e., $u \cdot a = 1 \leftrightarrow u^{-1} = a$.

Units.inv_unique theorem

{u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹

Full source

@[to_additive]
theorem inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
  Units.inv_eq_of_mul_eq_one_right <| by rw [h, u₂.mul_inv]

Uniqueness of Inverses for Equal Units

Informal description

Let $u_1$ and $u_2$ be units in a monoid $\alpha$. If the underlying elements of $u_1$ and $u_2$ are equal (i.e., $u_1 = u_2$), then their inverses are also equal (i.e., $u_1^{-1} = u_2^{-1}$).

divp_left_inj theorem

(u : αˣ) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b

Full source

@[simp]
theorem divp_left_inj (u : αˣ) {a b : α} : a /ₚ ua /ₚ u = b /ₚ u ↔ a = b :=
  Units.mul_left_inj _

Left Cancellation Property for Division by a Unit

Informal description

Let $u$ be a unit (invertible element) in a monoid $\alpha$, and let $a, b$ be elements of $\alpha$. Then $a / u = b / u$ if and only if $a = b$.

divp_eq_iff_mul_eq theorem

{x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x

Full source

@[field_simps 1010]
theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ ux /ₚ u = y ↔ y * u = x :=
  u.mul_left_inj.symm.trans <| by rw [divp_mul_cancel]; exact ⟨Eq.symm, Eq.symm⟩

Division by Unit Equivalence: $x / u = y \leftrightarrow y \cdot u = x$

Informal description

For elements $x, y$ in a monoid $\alpha$ and a unit $u \in \alpha^\times$, the equation $x / u = y$ holds if and only if $y \cdot u = x$.

divp_eq_one_iff_eq theorem

{a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = u

Full source

theorem divp_eq_one_iff_eq {a : α} {u : αˣ} : a /ₚ ua /ₚ u = 1 ↔ a = u :=
  (Units.mul_left_inj u).symm.trans <| by rw [divp_mul_cancel, one_mul]

Division by Unit Yields One if and only if Equal to Unit

Informal description

For an element $a$ in a monoid $\alpha$ and a unit $u \in \alpha^\times$, the equation $a / u = 1$ holds if and only if $a = u$.

inv_eq_one_divp' theorem

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

Full source

/-- Used for `field_simp` to deal with inverses of units. This form of the lemma
is essential since `field_simp` likes to use `inv_eq_one_div` to rewrite
`↑u⁻¹ = ↑(1 / u)`. -/
@[field_simps]
theorem inv_eq_one_divp' (u : αˣ) : ((1 / u : αˣ) : α) = 1 /ₚ u := by
  rw [one_div, one_divp]

Inverse of Unit as Division of One by Unit

Informal description

For any unit $u$ in a monoid $\alpha$, the inverse of $u$ (as an element of $\alpha$) is equal to the division of $1$ by $u$ (using the division operation $\div_p$ for units), i.e., $u^{-1} = 1 \div_p u$.

LeftCancelMonoid.mul_eq_one theorem

: a * b = 1 ↔ a = 1 ∧ b = 1

Full source

@[to_additive (attr := simp)]
protected theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨LeftCancelMonoid.eq_one_of_mul_right h, LeftCancelMonoid.eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Product Equals Identity in Left Cancel Monoid if and Only if Both Factors Are Identity

Informal description

For any elements $a$ and $b$ in a left cancel monoid, the product $a \cdot b$ equals the identity element $1$ if and only if both $a$ and $b$ are equal to $1$.

LeftCancelMonoid.mul_ne_one theorem

: a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Full source

@[to_additive]
protected theorem mul_ne_one : a * b ≠ 1a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1 := by rw [not_iff_comm]; simp

Product Not Equal to Identity in Left Cancel Monoid if and Only if Either Factor is Not Identity

Informal description

For any elements $a$ and $b$ in a left cancel monoid, the product $a \cdot b$ is not equal to the identity element $1$ if and only if either $a \neq 1$ or $b \neq 1$.

RightCancelMonoid.mul_eq_one theorem

: a * b = 1 ↔ a = 1 ∧ b = 1

Full source

@[to_additive (attr := simp)]
protected theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨RightCancelMonoid.eq_one_of_mul_right h, RightCancelMonoid.eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Product Equals Identity in Right Cancel Monoid

Informal description

For elements $a$ and $b$ in a right cancel monoid, the product $a * b$ equals the identity element $1$ if and only if both $a$ and $b$ are equal to $1$.

RightCancelMonoid.mul_ne_one theorem

: a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Full source

@[to_additive]
protected theorem mul_ne_one : a * b ≠ 1a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1 := by rw [not_iff_comm]; simp

Product Not Equal to Identity in Right Cancel Monoid: $a * b \neq 1 \leftrightarrow a \neq 1 \lor b \neq 1$

Informal description

For elements $a$ and $b$ in a right cancel monoid, the product $a * b$ is not equal to the identity element $1$ if and only if either $a \neq 1$ or $b \neq 1$.

mul_eq_one' theorem

: a * b = 1 ↔ a = 1 ∧ b = 1

Full source

@[to_additive]
theorem mul_eq_one' : a * b = 1 ↔ a = 1 ∧ b = 1 := LeftCancelMonoid.mul_eq_one

Product Equals Identity if and Only if Both Factors Are Identity

Informal description

For any elements $a$ and $b$ in a monoid, the product $a \cdot b$ equals the identity element $1$ if and only if both $a = 1$ and $b = 1$.

mul_ne_one' theorem

: a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Full source

@[to_additive]
theorem mul_ne_one' : a * b ≠ 1a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1 := LeftCancelMonoid.mul_ne_one

Product Not Equal to Identity in Monoid if and Only if Either Factor is Not Identity

Informal description

For any elements $a$ and $b$ in a monoid, the product $a \cdot b$ is not equal to the identity element $1$ if and only if either $a \neq 1$ or $b \neq 1$.

divp_mul_eq_mul_divp theorem

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

Full source

@[field_simps]
theorem divp_mul_eq_mul_divp (x y : α) (u : αˣ) : x /ₚ u * y = x * y /ₚ u := by
  rw [divp, divp, mul_right_comm]

Right Multiplication by Unit Preserves Division: $(x / u) \cdot y = (x \cdot y) / u$

Informal description

For any elements $x, y$ in a monoid $\alpha$ and any unit $u$ of $\alpha$, the following equality holds: $(x / u) \cdot y = (x \cdot y) / u$.

divp_eq_divp_iff theorem

{x y : α} {ux uy : αˣ} : x /ₚ ux = y /ₚ uy ↔ x * uy = y * ux

Full source

@[field_simps]
theorem divp_eq_divp_iff {x y : α} {ux uy : αˣ} : x /ₚ uxx /ₚ ux = y /ₚ uy ↔ x * uy = y * ux := by
  rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

Equality of Unit-Divided Elements: $x / u_x = y / u_y \leftrightarrow x \cdot u_y = y \cdot u_x$

Informal description

For any elements $x, y$ in a monoid $\alpha$ and any units $u_x, u_y$ of $\alpha$, the equality $x / u_x = y / u_y$ holds if and only if $x \cdot u_y = y \cdot u_x$.

divp_mul_divp theorem

(x y : α) (ux uy : αˣ) : x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

Full source

@[field_simps]
theorem divp_mul_divp (x y : α) (ux uy : αˣ) : x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy) := by
  rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]

Multiplication of Unit-Divided Elements: $(x / u_x) \cdot (y / u_y) = (x \cdot y) / (u_x \cdot u_y)$

Informal description

For any elements $x, y$ in a monoid $\alpha$ and any units $u_x, u_y$ of $\alpha$, the following equality holds: $(x / u_x) \cdot (y / u_y) = (x \cdot y) / (u_x \cdot u_y)$.

mul_eq_one theorem

: a * b = 1 ↔ a = 1 ∧ b = 1

Full source

@[to_additive (attr := simp)]
theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨eq_one_of_mul_right h, eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Product Equals One if and only if Both Factors Equal One

Informal description

For elements $a$ and $b$ in a monoid, the product $a * b$ equals the multiplicative identity $1$ if and only if both $a$ and $b$ equal $1$.

mul_ne_one theorem

: a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Full source

@[to_additive] theorem mul_ne_one : a * b ≠ 1a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1 := by rw [not_iff_comm]; simp

Product Not Equal to One if and only if At Least One Factor Not Equal to One

Informal description

For elements $a$ and $b$ in a monoid, the product $a \cdot b$ is not equal to the multiplicative identity $1$ if and only if either $a \neq 1$ or $b \neq 1$.

isUnit_of_subsingleton theorem

[Monoid M] [Subsingleton M] (a : M) : IsUnit a

Full source

@[to_additive (attr := nontriviality)]
theorem isUnit_of_subsingleton [Monoid M] [Subsingleton M] (a : M) : IsUnit a :=
  ⟨⟨a, a, by subsingleton, by subsingleton⟩, rfl⟩

In a Subsingleton Monoid, Every Element is a Unit

Informal description

For any monoid $M$ that is a subsingleton (i.e., all elements are equal) and any element $a \in M$, the element $a$ is a unit (i.e., invertible).

instCanLiftUnitsValIsUnit instance

[Monoid M] : CanLift M Mˣ Units.val IsUnit

Full source

@[to_additive]
instance [Monoid M] : CanLift M Mˣ Units.val IsUnit :=
  { prf := fun _ ↦ id }

Lifting Elements to Units via Valuation in a Monoid

Informal description

For any monoid $M$, there is a canonical way to lift an element of $M$ to a unit (invertible element) in $M^\times$ via the valuation map $\text{val} : M^\times \to M$, provided the element satisfies the condition of being a unit (i.e., having a two-sided inverse).

instUniqueUnitsOfSubsingleton instance

[Monoid M] [Subsingleton M] : Unique Mˣ

Full source

/-- A subsingleton `Monoid` has a unique unit. -/
@[to_additive "A subsingleton `AddMonoid` has a unique additive unit."]
instance [Monoid M] [Subsingleton M] : Unique Mˣ where
  uniq _ := Units.val_eq_one.mp (by subsingleton)

Uniqueness of Units in a Subsingleton Monoid

Informal description

For any monoid $M$ that is a subsingleton (i.e., all elements are equal), the set of units $M^\times$ has exactly one element.

units_eq_one theorem

[Subsingleton Mˣ] (u : Mˣ) : u = 1

Full source

theorem units_eq_one [Subsingleton Mˣ] (u : Mˣ) : u = 1 := by subsingleton

Units in a Subsingleton Monoid are Trivial

Informal description

For any monoid $M$ such that the type of units $M^\times$ is a subsingleton (i.e., all elements are equal), every unit $u \in M^\times$ is equal to the multiplicative identity $1$.

IsUnit.mul_left_inj theorem

(h : IsUnit a) : b * a = c * a ↔ b = c

Full source

@[to_additive]
theorem mul_left_inj (h : IsUnit a) : b * a = c * a ↔ b = c :=
  let ⟨u, hu⟩ := h
  hu ▸ u.mul_left_inj

Left Cancellation Property for Multiplication by a Unit: $b \cdot a = c \cdot a \leftrightarrow b = c$

Informal description

Let $a$ be an invertible element (unit) in a monoid, and let $b, c$ be arbitrary elements of the monoid. Then $b \cdot a = c \cdot a$ if and only if $b = c$.

IsUnit.mul_right_inj theorem

(h : IsUnit a) : a * b = a * c ↔ b = c

Full source

@[to_additive]
theorem mul_right_inj (h : IsUnit a) : a * b = a * c ↔ b = c :=
  let ⟨u, hu⟩ := h
  hu ▸ u.mul_right_inj

Right Cancellation Property for Multiplication by a Unit: $a \cdot b = a \cdot c \leftrightarrow b = c$

Informal description

Let $a$ be an invertible element (unit) in a monoid, and let $b, c$ be arbitrary elements of the monoid. Then $a \cdot b = a \cdot c$ if and only if $b = c$.

IsUnit.mul_left_cancel theorem

(h : IsUnit a) : a * b = a * c → b = c

Full source

@[to_additive]
protected theorem mul_left_cancel (h : IsUnit a) : a * b = a * c → b = c :=
  h.mul_right_inj.1

Left Cancellation Property for Multiplication by a Unit: $a \cdot b = a \cdot c \implies b = c$

Informal description

Let $a$ be an invertible element (unit) in a monoid, and let $b, c$ be arbitrary elements of the monoid. If $a \cdot b = a \cdot c$, then $b = c$.

IsUnit.mul_right_cancel theorem

(h : IsUnit b) : a * b = c * b → a = c

Full source

@[to_additive]
protected theorem mul_right_cancel (h : IsUnit b) : a * b = c * b → a = c :=
  h.mul_left_inj.1

Right Cancellation Property for Multiplication by a Unit: $a \cdot b = c \cdot b \implies a = c$

Informal description

Let $b$ be an invertible element (unit) in a monoid, and let $a, c$ be arbitrary elements of the monoid. If $a \cdot b = c \cdot b$, then $a = c$.

IsUnit.mul_eq_right theorem

(h : IsUnit b) : a * b = b ↔ a = 1

Full source

@[to_additive]
theorem mul_eq_right (h : IsUnit b) : a * b = b ↔ a = 1 := calc
  a * b = b ↔ a * b = 1 * b := by rw [one_mul]
    _ ↔ a = 1 := by rw [h.mul_left_inj]

Right Multiplication by Unit Equals Itself if and only if Left Factor is Identity: $a \cdot b = b \leftrightarrow a = 1$

Informal description

Let $b$ be an invertible element (unit) in a monoid, and let $a$ be an arbitrary element of the monoid. Then $a \cdot b = b$ if and only if $a$ is the multiplicative identity element $1$.

IsUnit.mul_eq_left theorem

(h : IsUnit a) : a * b = a ↔ b = 1

Full source

@[to_additive]
theorem mul_eq_left (h : IsUnit a) : a * b = a ↔ b = 1 := calc
  a * b = a ↔ a * b = a * 1 := by rw [mul_one]
    _ ↔ b = 1 := by rw [h.mul_right_inj]

Left Multiplication by Unit Equals Itself if and only if Right Factor is Identity: $a \cdot b = a \leftrightarrow b = 1$

Informal description

Let $a$ be an invertible element (unit) in a monoid, and let $b$ be an arbitrary element of the monoid. Then $a \cdot b = a$ if and only if $b$ is the multiplicative identity element $1$.

IsUnit.mul_right_injective theorem

(h : IsUnit a) : Injective (a * ·)

Full source

@[to_additive]
protected theorem mul_right_injective (h : IsUnit a) : Injective (a * ·) :=
  fun _ _ => h.mul_left_cancel

Right Multiplication by Unit is Injective: $x \mapsto x \cdot a$

Informal description

Let $a$ be an invertible element (unit) in a monoid. Then the right multiplication map $x \mapsto x \cdot a$ is injective.

IsUnit.mul_left_injective theorem

(h : IsUnit b) : Injective (· * b)

Full source

@[to_additive]
protected theorem mul_left_injective (h : IsUnit b) : Injective (· * b) :=
  fun _ _ => h.mul_right_cancel

Left Multiplication by Unit is Injective: $x \mapsto b \cdot x$

Informal description

Let $b$ be an invertible element (unit) in a monoid. Then the left multiplication map $x \mapsto b \cdot x$ is injective.

IsUnit.isUnit_iff_mulLeft_bijective theorem

{a : M} : IsUnit a ↔ Function.Bijective (a * ·)

Full source

@[to_additive]
theorem isUnit_iff_mulLeft_bijective {a : M} :
    IsUnitIsUnit a ↔ Function.Bijective (a * ·) :=
  ⟨fun h ↦ ⟨h.mul_right_injective, fun y ↦ ⟨h.unit⁻¹ * y, by simp [← mul_assoc]⟩⟩, fun h ↦
    ⟨⟨a, _, (h.2 1).choose_spec, h.1
      (by simpa [mul_assoc] using congr_arg (· * a) (h.2 1).choose_spec)⟩, rfl⟩⟩

Characterization of Units via Bijective Left Multiplication

Informal description

An element $a$ in a monoid $M$ is a unit if and only if the left multiplication map $x \mapsto a \cdot x$ is bijective.

IsUnit.isUnit_iff_mulRight_bijective theorem

{a : M} : IsUnit a ↔ Function.Bijective (· * a)

Full source

@[to_additive]
theorem isUnit_iff_mulRight_bijective {a : M} :
    IsUnitIsUnit a ↔ Function.Bijective (· * a) :=
  ⟨fun h ↦ ⟨h.mul_left_injective, fun y ↦ ⟨y * h.unit⁻¹, by simp [mul_assoc]⟩⟩,
    fun h ↦ ⟨⟨a, _, h.1 (by simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec),
      (h.2 1).choose_spec⟩, rfl⟩⟩

Characterization of Units via Bijective Right Multiplication

Informal description

An element $a$ in a monoid $M$ is a unit (i.e., has a two-sided inverse) if and only if the right multiplication map $x \mapsto x \cdot a$ is bijective.

IsUnit.mul_inv_cancel_right theorem

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

Full source

@[to_additive (attr := simp)]
protected lemma mul_inv_cancel_right (h : IsUnit b) (a : α) : a * b * b⁻¹ = a :=
  h.unit'.mul_inv_cancel_right _

Right multiplication by a unit and its inverse preserves the original element

Informal description

For any element $a$ in a monoid $\alpha$ and any invertible element $b$ (i.e., $b$ is a unit), the product $a \cdot b \cdot b^{-1}$ equals $a$.

IsUnit.inv_mul_cancel_right theorem

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

Full source

@[to_additive (attr := simp)]
protected lemma inv_mul_cancel_right (h : IsUnit b) (a : α) : a * b⁻¹ * b = a :=
  h.unit'.inv_mul_cancel_right _

Right cancellation property for invertible elements: $a * b^{-1} * b = a$

Informal description

For any element $a$ in a monoid $\alpha$ and any invertible element $b$ in $\alpha$, the operation $a * b^{-1} * b$ simplifies to $a$.

IsUnit.inv_mul_eq_iff_eq_mul theorem

(h : IsUnit a) : a⁻¹ * b = c ↔ b = a * c

Full source

@[to_additive]
protected lemma inv_mul_eq_iff_eq_mul (h : IsUnit a) : a⁻¹a⁻¹ * b = c ↔ b = a * c :=
  h.unit'.inv_mul_eq_iff_eq_mul

Invertible Element Property: $a^{-1}b = c \leftrightarrow b = ac$

Informal description

For any element $a$ in a division monoid that is invertible (i.e., `IsUnit a` holds), the equation $a^{-1} * b = c$ holds if and only if $b = a * c$.

IsUnit.mul_inv_eq_iff_eq_mul theorem

(h : IsUnit b) : a * b⁻¹ = c ↔ a = c * b

Full source

@[to_additive]
protected lemma mul_inv_eq_iff_eq_mul (h : IsUnit b) : a * b⁻¹ = c ↔ a = c * b :=
  h.unit'.mul_inv_eq_iff_eq_mul

Equivalence of right multiplication by inverse and original multiplication for invertible elements: $a \cdot b^{-1} = c \leftrightarrow a = c \cdot b$

Informal description

For any elements $a$ and $c$ in a monoid $\alpha$, and any invertible element $b$ in $\alpha$ (i.e., `IsUnit b` holds), the equation $a \cdot b^{-1} = c$ holds if and only if $a = c \cdot b$.

IsUnit.mul_inv_eq_one theorem

(h : IsUnit b) : a * b⁻¹ = 1 ↔ a = b

Full source

@[to_additive]
protected lemma mul_inv_eq_one (h : IsUnit b) : a * b⁻¹ = 1 ↔ a = b :=
  @Units.mul_inv_eq_one _ _ h.unit' _

Unit Condition: $a \cdot b^{-1} = 1 \leftrightarrow a = b$ for invertible $b$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is a unit (i.e., invertible), then the product $a \cdot b^{-1}$ equals the identity element $1$ if and only if $a = b$.

IsUnit.inv_mul_eq_one theorem

(h : IsUnit a) : a⁻¹ * b = 1 ↔ a = b

Full source

@[to_additive]
protected lemma inv_mul_eq_one (h : IsUnit a) : a⁻¹a⁻¹ * b = 1 ↔ a = b :=
  @Units.inv_mul_eq_one _ _ h.unit' _

Unit Condition: $a^{-1} \cdot b = 1 \leftrightarrow a = b$ for invertible $a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ is invertible (i.e., `IsUnit a` holds), then the product $a^{-1} \cdot b$ equals the identity element $1$ if and only if $a = b$.

IsUnit.mul_eq_one_iff_eq_inv theorem

(h : IsUnit b) : a * b = 1 ↔ a = b⁻¹

Full source

@[to_additive]
protected lemma mul_eq_one_iff_eq_inv (h : IsUnit b) : a * b = 1 ↔ a = b⁻¹ :=
  @Units.mul_eq_one_iff_eq_inv _ _ h.unit' _

Unit condition: $a \cdot b = 1 \leftrightarrow a = b^{-1}$ for invertible $b$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible (i.e., $b$ is a unit), then the product $a \cdot b$ equals the identity element $1$ if and only if $a$ is equal to the inverse of $b$.

IsUnit.mul_eq_one_iff_inv_eq theorem

(h : IsUnit a) : a * b = 1 ↔ a⁻¹ = b

Full source

@[to_additive]
protected lemma mul_eq_one_iff_inv_eq (h : IsUnit a) : a * b = 1 ↔ a⁻¹ = b :=
  @Units.mul_eq_one_iff_inv_eq _ _ h.unit' _

Unit condition: $a \cdot b = 1 \leftrightarrow a^{-1} = b$ for invertible $a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ is invertible (i.e., $a$ is a unit), then the product $a \cdot b$ equals the identity element $1$ if and only if the inverse of $a$ equals $b$, i.e., $a \cdot b = 1 \leftrightarrow a^{-1} = b$.

IsUnit.div_mul_cancel theorem

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

Full source

@[to_additive (attr := simp)]
protected lemma div_mul_cancel (h : IsUnit b) (a : α) : a / b * b = a := by
  rw [div_eq_mul_inv, h.inv_mul_cancel_right]

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

Informal description

For any element $a$ in a division monoid $\alpha$ and any invertible element $b$ (i.e., $b$ is a unit), the expression $(a / b) \cdot b$ simplifies to $a$.

IsUnit.mul_div_cancel_right theorem

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

Full source

@[to_additive (attr := simp)]
protected lemma mul_div_cancel_right (h : IsUnit b) (a : α) : a * b / b = a := by
  rw [div_eq_mul_inv, h.mul_inv_cancel_right]

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

Informal description

For any element $a$ in a division monoid $\alpha$ and any invertible element $b$ (i.e., $b$ is a unit), the expression $a \cdot b / b$ simplifies to $a$.

IsUnit.mul_one_div_cancel theorem

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

Full source

@[to_additive]
protected lemma mul_one_div_cancel (h : IsUnit a) : a * (1 / a) = 1 := by simp [h]

Invertible Element Property: $a \cdot (1/a) = 1$

Informal description

For any invertible element $a$ in a division monoid $\alpha$, the product of $a$ and $1/a$ equals the multiplicative identity, i.e., $a \cdot (1/a) = 1$.

IsUnit.one_div_mul_cancel theorem

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

Full source

@[to_additive]
protected lemma one_div_mul_cancel (h : IsUnit a) : 1 / a * a = 1 := by simp [h]

Inverse Property of Units: $(1 / a) \cdot a = 1$

Informal description

For any element $a$ in a division monoid $\alpha$, if $a$ is a unit (i.e., invertible), then $(1 / a) \cdot a = 1$.

IsUnit.div_left_inj theorem

(h : IsUnit c) : a / c = b / c ↔ a = b

Full source

@[to_additive]
protected lemma div_left_inj (h : IsUnit c) : a / c = b / c ↔ a = b := by
  simp only [div_eq_mul_inv]
  exact Units.mul_left_inj h.inv.unit'

Left Cancellation Property for Division by a Unit

Informal description

Let $c$ be an invertible element in a division monoid $\alpha$, and let $a, b$ be elements of $\alpha$. Then $a / c = b / c$ if and only if $a = b$.

IsUnit.div_eq_iff theorem

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

Full source

@[to_additive]
protected lemma div_eq_iff (h : IsUnit b) : a / b = c ↔ a = c * b := by
  rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]

Division by Unit Equals Multiplication: $a / b = c \leftrightarrow a = c \cdot b$

Informal description

For any elements $a$ and $c$ in a division monoid $\alpha$, and any invertible element $b$ in $\alpha$ (i.e., $b$ is a unit), the equation $a / b = c$ holds if and only if $a = c \cdot b$.

IsUnit.div_eq_of_eq_mul theorem

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

Full source

@[to_additive]
protected lemma div_eq_of_eq_mul (h : IsUnit b) : a = c * b → a / b = c :=
  h.div_eq_iff.2

Division by Unit Equals Multiplicative Factor: $a = c \cdot b \rightarrow a / b = c$

Informal description

For any elements $a$ and $c$ in a division monoid $\alpha$, and any invertible element $b$ in $\alpha$ (i.e., $b$ is a unit), if $a = c \cdot b$, then $a / b = c$.

IsUnit.div_eq_one_iff_eq theorem

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

Full source

@[to_additive]
protected lemma div_eq_one_iff_eq (h : IsUnit b) : a / b = 1 ↔ a = b :=
  ⟨eq_of_div_eq_one, fun hab => hab.symm ▸ h.div_self⟩

Division by Unit Equals One iff Elements Are Equal

Informal description

For any element $b$ in a division monoid $\alpha$ that is a unit (i.e., invertible), the equation $a / b = 1$ holds if and only if $a = b$.

IsUnit.div_mul_left theorem

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

Full source

@[to_additive]
protected lemma div_mul_left (h : IsUnit b) : b / (a * b) = 1 / a := by
  rw [h.div_mul_cancel_right, one_div]

Simplification of Division by a Unit: $b/(a \cdot b) = 1/a$

Informal description

For any element $b$ in a division monoid $\alpha$ that is a unit (i.e., invertible), the expression $b / (a \cdot b)$ simplifies to $1 / a$ for any element $a \in \alpha$.

IsUnit.mul_mul_div theorem

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

Full source

@[to_additive]
protected lemma mul_mul_div (a : α) (h : IsUnit b) : a * b * (1 / b) = a := by simp [h]

Simplification of Multiplication by Unit and its Inverse: $a \cdot b \cdot (1/b) = a$

Informal description

For any element $a$ in a division monoid $\alpha$ and any invertible element $b$ (i.e., $b$ is a unit), the expression $a \cdot b \cdot (1 / b)$ simplifies to $a$.

IsUnit.div_mul_right theorem

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

Full source

@[to_additive]
protected lemma div_mul_right (h : IsUnit a) (b : α) : a / (a * b) = 1 / b := by
  rw [mul_comm, h.div_mul_left]

Simplification of Division by a Unit: $a/(a \cdot b) = 1/b$

Informal description

For any invertible element $a$ in a division monoid $\alpha$ and any element $b \in \alpha$, the expression $a / (a \cdot b)$ simplifies to $1 / b$.

IsUnit.mul_div_cancel_left theorem

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

Full source

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

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

Informal description

For any invertible element $a$ in a division monoid $\alpha$ and any element $b \in \alpha$, the expression $a \cdot b / a$ simplifies to $b$.

IsUnit.mul_div_cancel theorem

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

Full source

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

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

Informal description

For any invertible element $a$ in a division monoid $\alpha$ and any element $b \in \alpha$, the expression $a \cdot (b / a)$ simplifies to $b$.

IsUnit.mul_eq_mul_of_div_eq_div theorem

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

Full source

@[to_additive]
protected lemma mul_eq_mul_of_div_eq_div (hb : IsUnit b) (hd : IsUnit d)
    (a c : α) (h : a / b = c / d) : a * d = c * b := by
  rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]

Cross-Multiplication Equality for Units: $\frac{a}{b} = \frac{c}{d} \implies a \cdot d = c \cdot b$

Informal description

For any elements $a, c$ in a division monoid $\alpha$ and any invertible elements $b, d$ (i.e., $b$ and $d$ are units), if $\frac{a}{b} = \frac{c}{d}$, then $a \cdot d = c \cdot b$.

IsUnit.div_eq_div_iff theorem

(hb : IsUnit b) (hd : IsUnit d) : a / b = c / d ↔ a * d = c * b

Full source

@[to_additive]
protected lemma div_eq_div_iff (hb : IsUnit b) (hd : IsUnit d) :
    a / b = c / d ↔ a * d = c * b := by
  rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]

Fraction Equality Criterion via Cross-Multiplication for Units: $\frac{a}{b} = \frac{c}{d} \leftrightarrow a \cdot d = c \cdot b$

Informal description

For any elements $a, c$ in a division monoid $\alpha$ and any invertible elements $b, d$ (i.e., $b$ and $d$ are units), the equality of fractions $\frac{a}{b} = \frac{c}{d}$ holds if and only if the cross-multiplication equality $a \cdot d = c \cdot b$ holds.

IsUnit.div_div_cancel theorem

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

Full source

@[to_additive]
protected lemma div_div_cancel (h : IsUnit a) : a / (a / b) = b := by
  rw [div_div_eq_mul_div, h.mul_div_cancel_left]

Double Division Cancellation for Units: $a/(a/b) = b$

Informal description

For any invertible element $a$ in a division monoid $\alpha$ and any element $b \in \alpha$, the expression $a / (a / b)$ simplifies to $b$.

IsUnit.div_div_cancel_left theorem

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

Full source

@[to_additive]
protected lemma div_div_cancel_left (h : IsUnit a) : a / b / a = b⁻¹ := by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

Double Division Cancellation for Units: $(a / b) / a = b^{-1}$

Informal description

For any element $a$ in a division monoid $\alpha$ such that $a$ is a unit, and for any element $b \in \alpha$, the following equality holds: $(a / b) / a = b^{-1}$.

TODO