Mathlib.Algebra.Group.Invertible.Defs

Module docstring

{"# Invertible elements

This file defines a typeclass Invertible a for elements a with a two-sided multiplicative inverse.

The intent of the typeclass is to provide a way to write e.g. ⅟2 in a ring like ℤ[1/2] where some inverses exist but there is no general ⁻¹ operator; or to specify that a field has characteristic ≠ 2. It is the Type-valued analogue to the Prop-valued IsUnit.

For constructions of the invertible element given a characteristic, see Algebra/CharP/Invertible and other lemmas in that file.

Notation

⅟a is Invertible.invOf a, the inverse of a

Implementation notes

The Invertible class lives in Type, not Prop, to make computation easier. If multiplication is associative, Invertible is a subsingleton anyway.

The simp normal form tries to normalize ⅟a to a ⁻¹. Otherwise, it pushes ⅟ inside the expression as much as possible.

Since Invertible a is not a Prop (but it is a Subsingleton), we have to be careful about coherence issues: we should avoid having multiple non-defeq instances for Invertible a in the same context. This file plays it safe and uses def rather than instance for most definitions, users can choose which instances to use at the point of use.

For example, here's how you can use an Invertible 1 instance: ```lean variable {α : Type*} [Monoid α]

def somethingthatneeds_inverses (x : α) [Invertible x] := sorry

section attribute [local instance] invertibleOne def somethingone := somethingthatneedsinverses 1 end ```

Typeclass search vs. unification for `simp` lemmas

Note that since typeclass search searches the local context first, an instance argument like [Invertible a] might sometimes be filled by a different term than the one we'd find by unification (i.e., the one that's used as an implicit argument to ⅟).

This can cause issues with simp. Therefore, some lemmas are duplicated, with the @[simp] versions using unification and the user-facing ones using typeclass search.

Since unification can make backwards rewriting (e.g. rw [← mylemma]) impractical, we still want the instance-argument versions; therefore the user-facing versions retain the instance arguments and the original lemma name, whereas the @[simp]/unification ones acquire a ' at the end of their name.

We modify this file according to the above pattern only as needed; therefore, most @[simp] lemmas here are not part of such a duplicate pair. This is not (yet) intended as a permanent solution.

See Zulip: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Invertible.201.20simps/near/320558233]

Tags

invertible, inverse element, invOf, a half, one half, a third, one third, ½, ⅓

Invertible structure

[Mul α] [One α] (a : α)

Full source

/-- `Invertible a` gives a two-sided multiplicative inverse of `a`. -/
class Invertible [Mul α] [One α] (a : α) : Type u where
  /-- The inverse of an `Invertible` element -/
  invOf : α
  /-- `invOf a` is a left inverse of `a` -/
  invOf_mul_self : invOf * a = 1
  /-- `invOf a` is a right inverse of `a` -/
  mul_invOf_self : a * invOf = 1

Invertible Element

Informal description

The structure `Invertible a` provides a two-sided multiplicative inverse for an element `a` in a type `α` equipped with multiplication and a one element.

term⅟_ definition

: Lean.ParserDescr✝

Full source

/-- The inverse of an `Invertible` element -/
-- This notation has the same precedence as `Inv.inv`.
prefix:max "⅟ " => Invertible.invOf

Inverse of an invertible element

Informal description

The notation `⅟a` represents the inverse of an element `a` that has a two-sided multiplicative inverse, i.e., an element for which the `Invertible` structure is defined.

invOf_mul_self' theorem

[Mul α] [One α] (a : α) {_ : Invertible a} : ⅟ a * a = 1

Full source

@[simp]
theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟ a * a = 1 :=
  Invertible.invOf_mul_self

Left Inverse Property: $⅟a \cdot a = 1$

Informal description

For any element $a$ in a multiplicative monoid with identity, if $a$ is invertible (i.e., there exists an element denoted by $⅟a$), then the product of $⅟a$ and $a$ equals the identity element, i.e., $⅟a \cdot a = 1$.

invOf_mul_self theorem

[Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1

Full source

theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1 := invOf_mul_self' _

Left Inverse Property: $⅟a \cdot a = 1$

Informal description

mul_invOf_self' theorem

[Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟ a = 1

Full source

@[simp]
theorem mul_invOf_self' [Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟ a = 1 :=
  Invertible.mul_invOf_self

Right Inverse Property: $a \cdot ⅟a = 1$

Informal description

For any element $a$ in a multiplicative monoid with identity, if $a$ is invertible (i.e., there exists an element denoted by $⅟a$), then the product of $a$ and $⅟a$ equals the identity element, i.e., $a \cdot ⅟a = 1$.

mul_invOf_self theorem

[Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1

Full source

theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1 := mul_invOf_self' _

Right Inverse Property: $a \cdot ⅟a = 1$

Informal description

invOf_mul_cancel_left' theorem

[Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b

Full source

@[simp]
theorem invOf_mul_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b := by
  rw [← mul_assoc, invOf_mul_self, one_mul]

Left cancellation property of invertible elements: $⅟a \cdot (a \cdot b) = b$

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$. If $a$ is invertible with inverse $⅟a$, then $⅟a \cdot (a \cdot b) = b$.

invOf_mul_cancel_left theorem

[Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b

Full source

theorem invOf_mul_cancel_left [Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b :=
  invOf_mul_cancel_left' _ _

Left cancellation property of invertible elements: $⅟a \cdot (a \cdot b) = b$

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$. If $a$ is invertible with inverse $⅟a$, then $⅟a \cdot (a \cdot b) = b$.

mul_invOf_cancel_left' theorem

[Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b

Full source

@[simp]
theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b := by
  rw [← mul_assoc, mul_invOf_self, one_mul]

Left Cancellation via Invertible Element: $a \cdot (⅟a \cdot b) = b$

Informal description

Let $a$ and $b$ be elements of a monoid $\alpha$, and suppose $a$ is invertible with inverse $⅟a$. Then $a \cdot (⅟a \cdot b) = b$.

mul_invOf_cancel_left theorem

[Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b

Full source

theorem mul_invOf_cancel_left [Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b :=
  mul_invOf_cancel_left' a b

Left Cancellation Property via Invertible Element

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$ with $a$ invertible. Then $a \cdot (⅟a \cdot b) = b$.

invOf_mul_cancel_right' theorem

[Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a

Full source

@[simp]
theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a := by
  simp [mul_assoc]

Right Cancellation Property: $a \cdot ⅟b \cdot b = a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible (i.e., there exists an element $⅟b$), then the product $a \cdot ⅟b \cdot b$ equals $a$.

invOf_mul_cancel_right theorem

[Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a

Full source

theorem invOf_mul_cancel_right [Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a :=
  invOf_mul_cancel_right' _ _

Right Cancellation Property via Invertible Element: $a \cdot ⅟b \cdot b = a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible with inverse $⅟b$, then the product $a \cdot ⅟b \cdot b$ equals $a$.

mul_invOf_cancel_right' theorem

[Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a

Full source

@[simp]
theorem mul_invOf_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a := by
  simp [mul_assoc]

Right Cancellation Property via Invertible Element: $(a \cdot b) \cdot ⅟b = a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible with inverse $⅟b$, then $(a \cdot b) \cdot ⅟b = a$.

mul_invOf_cancel_right theorem

[Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a

Full source

theorem mul_invOf_cancel_right [Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a :=
  mul_invOf_cancel_right' _ _

Right Cancellation Property via Invertible Element: $(a \cdot b) \cdot ⅟b = a$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $b$ is invertible with inverse $⅟b$, then $(a \cdot b) \cdot ⅟b = a$.

invOf_eq_right_inv theorem

[Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟ a = b

Full source

theorem invOf_eq_right_inv [Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟ a = b :=
  left_inv_eq_right_inv (invOf_mul_self _) hac

Right Inverse Characterizes Invertible Element: $⅟a = b$ when $a \cdot b = 1$

Informal description

Let $a$ and $b$ be elements of a monoid $\alpha$. If $a$ is invertible and $a \cdot b = 1$, then the inverse of $a$ (denoted $⅟a$) is equal to $b$.

invOf_eq_left_inv theorem

[Monoid α] {a b : α} [Invertible a] (hac : b * a = 1) : ⅟ a = b

Full source

theorem invOf_eq_left_inv [Monoid α] {a b : α} [Invertible a] (hac : b * a = 1) : ⅟ a = b :=
  (left_inv_eq_right_inv hac (mul_invOf_self _)).symm

Right inverse equals left inverse in a monoid

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$. If $a$ is invertible and $b$ is a left inverse of $a$ (i.e., $b \cdot a = 1$), then the right inverse $⅟a$ equals $b$.

invertible_unique theorem

{α : Type u} [Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) : ⅟ a = ⅟ b

Full source

theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [Invertible b]
    (h : a = b) : ⅟ a = ⅟ b := by
  apply invOf_eq_right_inv
  rw [h, mul_invOf_self]

Uniqueness of Inverses for Equal Elements in a Monoid

Informal description

Let $\alpha$ be a monoid and let $a, b \in \alpha$ be invertible elements. If $a = b$, then their inverses are equal, i.e., $⅟a = ⅟b$.

Invertible.subsingleton instance

[Monoid α] (a : α) : Subsingleton (Invertible a)

Full source

instance Invertible.subsingleton [Monoid α] (a : α) : Subsingleton (Invertible a) :=
  ⟨fun ⟨b, hba, hab⟩ ⟨c, _, hac⟩ => by
    congr
    exact left_inv_eq_right_inv hba hac⟩

Uniqueness of Invertibility Proofs

Informal description

For any monoid $\alpha$ and element $a \in \alpha$, the type `Invertible a` of proofs that $a$ has a two-sided multiplicative inverse is a subsingleton (i.e., any two such proofs are equal).

Invertible.congr theorem

[Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) : ⅟ a = ⅟ b

Full source

/-- If `a` is invertible and `a = b`, then `⅟a = ⅟b`. -/
@[congr]
theorem Invertible.congr [Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) :
    ⅟a = ⅟b := by subst h; congr; apply Subsingleton.allEq

Inverse Equality under Element Equality in a Monoid

Informal description

Let $\alpha$ be a monoid, and let $a, b \in \alpha$ be invertible elements. If $a = b$, then their inverses are equal, i.e., $\text{⅟}a = \text{⅟}b$.

Invertible.copy' definition

[MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r) (hsi : si = ⅟ r) : Invertible s

Full source

/-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`. -/
def Invertible.copy' [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r)
    (hsi : si = ⅟ r) : Invertible s where
  invOf := si
  invOf_mul_self := by rw [hs, hsi, invOf_mul_self]
  mul_invOf_self := by rw [hs, hsi, mul_invOf_self]

Invertible element copy with explicit inverse

Informal description

Given a type $\alpha$ with multiplication and a one element, if $r$ is invertible with inverse $\text{⅟}r$, and $s = r$ and $si = \text{⅟}r$, then $s$ is invertible with inverse $\text{⅟}s = si$.

Invertible.copy abbrev

[MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) : Invertible s

Full source

/-- If `r` is invertible and `s = r`, then `s` is invertible. -/
abbrev Invertible.copy [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) :
    Invertible s :=
  hr.copy' _ _ hs rfl

Invertibility Preserved by Equality in a Monoid

Informal description

Given a monoid $\alpha$ with multiplication and a one element, if $r \in \alpha$ is invertible and $s \in \alpha$ satisfies $s = r$, then $s$ is invertible.

invertibleOfGroup definition

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

Full source

/-- Each element of a group is invertible. -/
def invertibleOfGroup [Group α] (a : α) : Invertible a :=
  ⟨a⁻¹, inv_mul_cancel a, mul_inv_cancel a⟩

Invertibility of group elements

Informal description

For any element $a$ in a group $\alpha$, $a$ is invertible with inverse $a^{-1}$.

invOf_eq_group_inv theorem

[Group α] (a : α) [Invertible a] : ⅟ a = a⁻¹

Full source

@[simp]
theorem invOf_eq_group_inv [Group α] (a : α) [Invertible a] : ⅟ a = a⁻¹ :=
  invOf_eq_right_inv (mul_inv_cancel a)

Invertible Inverse Equals Group Inverse: $⅟a = a^{-1}$ in a Group

Informal description

For any element $a$ in a group $\alpha$ with an `Invertible a` instance, the inverse element $⅟a$ is equal to the group inverse $a^{-1}$.

invertibleOne definition

[Monoid α] : Invertible (1 : α)

Full source

/-- `1` is the inverse of itself -/
def invertibleOne [Monoid α] : Invertible (1 : α) :=
  ⟨1, mul_one _, one_mul _⟩

Invertibility of the identity element

Informal description

In any monoid $\alpha$, the element $1$ is invertible with itself as the two-sided multiplicative inverse.

invOf_one' theorem

[Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1

Full source

@[simp]
theorem invOf_one' [Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1 :=
  invOf_eq_right_inv (mul_one _)

Inverse of Identity Equals Identity

Informal description

In any monoid $\alpha$, if the identity element $1$ is invertible, then its inverse $⅟1$ is equal to $1$.

invOf_one theorem

[Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1

Full source

theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 := invOf_one'

Inverse of Identity Equals Identity

Informal description

In any monoid $\alpha$ where the identity element $1$ is invertible, the inverse of $1$ is itself, i.e., $⅟1 = 1$.

invertibleInvOf instance

[One α] [Mul α] {a : α} [Invertible a] : Invertible (⅟ a)

Full source

/-- `a` is the inverse of `⅟a`. -/
instance invertibleInvOf [One α] [Mul α] {a : α} [Invertible a] : Invertible (⅟ a) :=
  ⟨a, mul_invOf_self a, invOf_mul_self a⟩

Invertibility of the Inverse Element

Informal description

For any element $a$ in a multiplicative monoid with identity, if $a$ is invertible with inverse $⅟a$, then $⅟a$ is also invertible with inverse $a$.

invOf_invOf theorem

[Monoid α] (a : α) [Invertible a] [Invertible (⅟ a)] : ⅟ (⅟ a) = a

Full source

@[simp]
theorem invOf_invOf [Monoid α] (a : α) [Invertible a] [Invertible (⅟ a)] : ⅟ (⅟ a) = a :=
  invOf_eq_right_inv (invOf_mul_self _)

Double Inverse Property: $⅟(⅟a) = a$

Informal description

For any element $a$ in a monoid $\alpha$ that is invertible with inverse $⅟a$, and where $⅟a$ is also invertible, the inverse of $⅟a$ is equal to $a$, i.e., $⅟(⅟a) = a$.

invOf_inj theorem

[Monoid α] {a b : α} [Invertible a] [Invertible b] : ⅟ a = ⅟ b ↔ a = b

Full source

@[simp]
theorem invOf_inj [Monoid α] {a b : α} [Invertible a] [Invertible b] : ⅟ a⅟ a = ⅟ b ↔ a = b :=
  ⟨invertible_unique _ _, invertible_unique _ _⟩

Inverse Equality Condition: $⅟a = ⅟b \leftrightarrow a = b$

Informal description

For any invertible elements $a$ and $b$ in a monoid $\alpha$, the equality of their inverses $⅟a = ⅟b$ holds if and only if $a = b$.

invertibleMul definition

[Monoid α] (a b : α) [Invertible a] [Invertible b] : Invertible (a * b)

Full source

/-- `⅟b * ⅟a` is the inverse of `a * b` -/
def invertibleMul [Monoid α] (a b : α) [Invertible a] [Invertible b] : Invertible (a * b) :=
  ⟨⅟ b * ⅟ a, by simp [← mul_assoc], by simp [← mul_assoc]⟩

Invertibility of the product of invertible elements

Informal description

For any elements $ a $ and $ b $ in a monoid $ \alpha $ that are invertible (i.e., have two-sided multiplicative inverses), the product $ a \cdot b $ is also invertible, with its inverse given by $ \text{⅟}(b) \cdot \text{⅟}(a) $.

invOf_mul theorem

[Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertible (a * b)] : ⅟ (a * b) = ⅟ b * ⅟ a

Full source

@[simp]
theorem invOf_mul [Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertible (a * b)] :
    ⅟ (a * b) = ⅟ b * ⅟ a :=
  invOf_eq_right_inv (by simp [← mul_assoc])

Inverse of Product Formula: $⅟(a \cdot b) = ⅟b \cdot ⅟a$

Informal description

Let $a$ and $b$ be elements of a monoid $\alpha$ such that $a$, $b$, and their product $a \cdot b$ are all invertible. Then the inverse of $a \cdot b$ is equal to the product of the inverses of $b$ and $a$, i.e., $⅟(a \cdot b) = ⅟b \cdot ⅟a$.

Invertible.mul abbrev

[Monoid α] {a b : α} (_ : Invertible a) (_ : Invertible b) : Invertible (a * b)

Full source

/-- A copy of `invertibleMul` for dot notation. -/
abbrev Invertible.mul [Monoid α] {a b : α} (_ : Invertible a) (_ : Invertible b) :
    Invertible (a * b) :=
  invertibleMul _ _

Invertibility of Product of Invertible Elements in a Monoid

Informal description

Given a monoid $\alpha$ and elements $a, b \in \alpha$ that are invertible, their product $a \cdot b$ is also invertible.

mul_left_inj_of_invertible theorem

: a * c = b * c ↔ a = b

Full source

theorem mul_left_inj_of_invertible : a * c = b * c ↔ a = b :=
  ⟨fun h => by simpa using congr_arg (· * ⅟c) h, congr_arg (· * _)⟩

Left Cancellation Property for Invertible Elements: $a \cdot c = b \cdot c \leftrightarrow a = b$

Informal description

For any elements $a$, $b$, and $c$ in a monoid, if $c$ is invertible, then $a \cdot c = b \cdot c$ if and only if $a = b$.

mul_right_inj_of_invertible theorem

: c * a = c * b ↔ a = b

Full source

theorem mul_right_inj_of_invertible : c * a = c * b ↔ a = b :=
  ⟨fun h => by simpa using congr_arg (⅟c * ·) h, congr_arg (_ * ·)⟩

Right Cancellation Property for Invertible Elements: $c \cdot a = c \cdot b \leftrightarrow a = b$

Informal description

Let $\alpha$ be a monoid and let $a, b, c \in \alpha$. If $c$ is invertible, then $c \cdot a = c \cdot b$ if and only if $a = b$.

invOf_mul_eq_iff_eq_mul_left theorem

: ⅟ c * a = b ↔ a = c * b

Full source

theorem invOf_mul_eq_iff_eq_mul_left : ⅟c⅟c * a = b ↔ a = c * b := by
  rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]

Left Inverse Multiplication Equivalence: $⅟c \cdot a = b \leftrightarrow a = c \cdot b$

Informal description

For any elements $a$, $b$, and $c$ in a monoid, where $c$ is invertible with inverse $⅟c$, the equation $⅟c \cdot a = b$ holds if and only if $a = c \cdot b$.

mul_left_eq_iff_eq_invOf_mul theorem

: c * a = b ↔ a = ⅟ c * b

Full source

theorem mul_left_eq_iff_eq_invOf_mul : c * a = b ↔ a = ⅟c * b := by
  rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]

Left Multiplication by Invertible Element is Equivalent to Left Multiplication by its Inverse: $c \cdot a = b \leftrightarrow a = ⅟c \cdot b$

Informal description

Let $\alpha$ be a monoid and let $a, b, c \in \alpha$. If $c$ is invertible with inverse $⅟c$, then $c \cdot a = b$ if and only if $a = ⅟c \cdot b$.

mul_invOf_eq_iff_eq_mul_right theorem

: a * ⅟ c = b ↔ a = b * c

Full source

theorem mul_invOf_eq_iff_eq_mul_right : a * ⅟c = b ↔ a = b * c := by
  rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]

Right Inverse Multiplication Equivalence: $a \cdot ⅟c = b \leftrightarrow a = b \cdot c$

Informal description

For any elements $a$, $b$, and $c$ in a monoid, where $c$ is invertible with inverse $⅟c$, the equation $a \cdot ⅟c = b$ holds if and only if $a = b \cdot c$.

mul_right_eq_iff_eq_mul_invOf theorem

: a * c = b ↔ a = b * ⅟ c

Full source

theorem mul_right_eq_iff_eq_mul_invOf : a * c = b ↔ a = b * ⅟c := by
  rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]

Right Multiplication by Invertible Element is Equivalent to Right Multiplication by its Inverse: $a \cdot c = b \leftrightarrow a = b \cdot ⅟c$

Informal description

For any elements $a$, $b$, and $c$ in a monoid, where $c$ is invertible with inverse $⅟c$, the equation $a \cdot c = b$ holds if and only if $a = b \cdot ⅟c$.

Notation

Implementation notes

Typeclass search vs. unification for simp lemmas

Tags

Typeclass search vs. unification for `simp` lemmas