Module docstring

{"# Typeclasses for algebraic operations

Notation typeclass for Inv, the multiplicative analogue of Neg.

We also introduce notation classes SMul and VAdd for multiplicative and additive actions.

SMul is typically, but not exclusively, used for scalar multiplication-like operators. See the module Algebra.AddTorsor for a motivating example for the name VAdd (vector addition).

Note Zero has already been defined in core Lean.

Notation

a • b is used as notation for HSMul.hSMul a b.
a +ᵥ b is used as notation for HVAdd.hVAdd a b.

","We have a macro to make x • y notation participate in the expression tree elaborator, like other arithmetic expressions such as +, *, /, ^, =, inequalities, etc. The macro is using the leftact% elaborator introduced in this RFC.

As a concrete example of the effect of this macro, consider ```lean variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)

check m + r • n

``Without the macro, the expression would elaborate asm + ↑(r • n : ↑N) : M. With the macro, the expression elaborates asm + r • (↑n : M) : M. To get the first interpretation, one can writem + (r • n :)`.

Here is a quick review of the expression tree elaborator: 1. It builds up an expression tree of all the immediately accessible operations that are marked with binop%, unop%, leftact%, rightact%, binrel%, etc. 2. It elaborates every leaf term of this tree (without an expected type, so as if it were temporarily wrapped in (... :)). 3. Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists. 4. It inserts coercions around leaf terms wherever needed.

The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.

Note(kmill): If we were to remove HSMul and switch to using SMul directly, then the expression tree elaborator would not be able to insert coercions within the right operand; they would likely appear as ↑(x • y) rather than x • ↑y, unlike other arithmetic operations. "}

HVAdd structure

(α : Type u) (β : Type v) (γ : outParam (Type w))

Full source

/--
The notation typeclass for heterogeneous additive actions.
This enables the notation `a +ᵥ b : γ` where `a : α`, `b : β`.
-/
class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a +ᵥ b` computes the sum of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hVAdd : α → β → γ

Heterogeneous Additive Action

Informal description

The structure representing a heterogeneous additive action, enabling the notation `a +ᵥ b : γ` where `a : α` and `b : β`. This is used to model operations where the types of the operands and the result can differ, such as vector addition in different spaces.

HSMul structure

(α : Type u) (β : Type v) (γ : outParam (Type w))

Full source

/--
The notation typeclass for heterogeneous scalar multiplication.
This enables the notation `a • b : γ` where `a : α`, `b : β`.

It is assumed to represent a left action in some sense.
The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action.
Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b`
when calculating the type of the surrounding arithmetic expression
and it tries to insert coercions into `b` to get some `b'`
such that `a • b'` has the same type as `b'`.
See the module documentation near the macro for more details.
-/
class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a • b` computes the product of `a` and `b`.
  The meaning of this notation is type-dependent, but it is intended to be used for left actions. -/
  hSMul : α → β → γ

Heterogeneous Scalar Multiplication

Informal description

The structure representing heterogeneous scalar multiplication, enabling the notation `a • b : γ` where `a : α` and `b : β`. This notation is assumed to represent a left action in some sense. The elaboration process for this notation focuses on the right operand `b`, using its type to determine the type of the surrounding arithmetic expression and attempting to insert coercions into `b` to ensure type consistency.

VAdd structure

(G : Type u) (P : Type v)

Full source

/-- Type class for the `+ᵥ` notation. -/
class VAdd (G : Type u) (P : Type v) where
  /-- `a +ᵥ b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent,
  but it is intended to be used for left actions. -/
  vadd : G → P → P

Vector Addition Type Class

Informal description

The structure representing the type class for the vector addition notation `+ᵥ`, which is used to denote additive actions between elements of types `G` and `P`.

VSub structure

(G : outParam Type*) (P : Type*)

Full source

/-- Type class for the `-ᵥ` notation. -/
class VSub (G : outParam Type*) (P : Type*) where
  /-- `a -ᵥ b` computes the difference of `a` and `b`. The meaning of this notation is
  type-dependent, but it is intended to be used for additive torsors. -/
  vsub : P → P → G

Vector Subtraction Type Class

Informal description

The structure representing the type class for the vector subtraction notation `-ᵥ`. It is used to define operations where elements of type `P` can be subtracted by elements of type `G`, with the result being of type `G`.

SMul structure

(M : Type u) (α : Type v)

Full source

/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
@[to_additive (attr := ext)]
class SMul (M : Type u) (α : Type v) where
  /-- `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent,
  but it is intended to be used for left actions. -/
  smul : M → α → α

Scalar Multiplication Typeclass

Informal description

The structure representing a typeclass for types equipped with a scalar multiplication operation, denoted by `•` (`\bu`). This operation takes an element of type `M` (the scalar) and an element of type `α` (the vector space or module element) and returns another element of type `α`.

term_+ᵥ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixr:65 " +ᵥ " => HVAdd.hVAdd

Vector addition notation

Informal description

The notation `+ᵥ` is defined as an infix operator with right associativity and precedence level 65, representing the operation `HVAdd.hVAdd` for vector addition. This notation is used to denote additive actions in algebraic structures.

term_-ᵥ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixl:65 " -ᵥ " => VSub.vsub

Vector subtraction notation

Informal description

The infix notation `-ᵥ` represents the vector subtraction operation `VSub.vsub`, which subtracts two vectors element-wise. The notation has left associativity and precedence level 65.

term_•_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixr:73 " • " => HSMul.hSMul

Scalar multiplication notation

Informal description

The notation `•` is defined as an infix operator with right associativity and precedence 73, representing the operation `HSMul.hSMul`. This notation is used for scalar multiplication-like operations in algebraic structures.

instHSMul instance

{α β} [SMul α β] : HSMul α β β

Full source

@[to_additive (attr := default_instance)]
instance instHSMul {α β} [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

Canonical Heterogeneous Scalar Multiplication from Scalar Multiplication

Informal description

For any types $\alpha$ and $\beta$ equipped with a scalar multiplication operation $\alpha \times \beta \to \beta$, there is a canonical heterogeneous scalar multiplication structure $\alpha \times \beta \to \beta$ that matches the given scalar multiplication.

SMul.smul_eq_hSMul theorem

{α β} [SMul α β] : (SMul.smul : α → β → β) = HSMul.hSMul

Full source

@[to_additive]
theorem SMul.smul_eq_hSMul {α β} [SMul α β] : (SMul.smul : α → β → β) = HSMul.hSMul := rfl

Equality of Scalar Multiplication and Heterogeneous Scalar Multiplication

Informal description

For any types $\alpha$ and $\beta$ equipped with a scalar multiplication operation `SMul.smul : α → β → β`, the scalar multiplication operation is equal to the heterogeneous scalar multiplication operation `HSMul.hSMul : α → β → β`.

Inv structure

(α : Type u)

Full source

/-- Class of types that have an inversion operation. -/
@[to_additive, notation_class]
class Inv (α : Type u) where
  /-- Invert an element of α, denoted by `a⁻¹`. -/
  inv : α → α

Inversion operation

Informal description

The structure `Inv` represents types equipped with an inversion operation, denoted by $x^{-1}$ for an element $x$ of the type. This operation is the multiplicative analogue of the additive negation operation `Neg`.

term_⁻¹ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
postfix:max "⁻¹" => Inv.inv

Multiplicative inverse notation

Informal description

The notation `x⁻¹` denotes the multiplicative inverse of `x` in a type equipped with an `Inv` instance.

mul_dite theorem

(a : α) (b : P → α) (c : ¬P → α) : (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Full source

@[to_additive]
lemma mul_dite (a : α) (b : P → α) (c : ¬ P → α) :
    (a * if h : P then b h else c h) = if h : P then a * b h else a * c h := by split <;> rfl

Multiplication Distributes Over Dependent Conditional Expression

Informal description

For any element $a$ in a type $\alpha$ with a multiplication operation, and for any functions $b : P \to \alpha$ and $c : \neg P \to \alpha$, the product of $a$ with a conditional expression (defined using `dite`) distributes as follows: $$ a \cdot \left(\text{if } h : P \text{ then } b(h) \text{ else } c(h)\right) = \text{if } h : P \text{ then } a \cdot b(h) \text{ else } a \cdot c(h). $$

mul_ite theorem

(a b c : α) : (a * if P then b else c) = if P then a * b else a * c

Full source

@[to_additive]
lemma mul_ite (a b c : α) : (a * if P then b else c) = if P then a * b else a * c := mul_dite ..

Multiplication Distributes Over Conditional Expression

Informal description

For any elements $a, b, c$ in a type $\alpha$ with a multiplication operation and any proposition $P$, the product of $a$ with a conditional expression distributes as follows: $$ a \cdot (\text{if } P \text{ then } b \text{ else } c) = \text{if } P \text{ then } a \cdot b \text{ else } a \cdot c. $$

dite_mul theorem

(a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Full source

@[to_additive]
lemma dite_mul (a : P → α) (b : ¬ P → α) (c : α) :
    (if h : P then a h else b h) * c = if h : P then a h * c else b h * c := by split <;> rfl

Multiplication of Conditional Expression by Scalar

Informal description

Let $P$ be a proposition, and let $a : P \to \alpha$, $b : \neg P \to \alpha$, and $c : \alpha$ be functions or elements of a type $\alpha$ with a multiplication operation. Then \[ \left(\text{if } h : P \text{ then } a(h) \text{ else } b(h)\right) \cdot c = \text{if } h : P \text{ then } a(h) \cdot c \text{ else } b(h) \cdot c. \]

ite_mul theorem

(a b c : α) : (if P then a else b) * c = if P then a * c else b * c

Full source

@[to_additive]
lemma ite_mul (a b c : α) : (if P then a else b) * c = if P then a * c else b * c := dite_mul ..

Conditional Multiplication: $(if\ P\ then\ a\ else\ b) \cdot c = if\ P\ then\ a \cdot c\ else\ b \cdot c$

Informal description

For any elements $a, b, c$ of a type $\alpha$ with a multiplication operation and any proposition $P$, the product of the conditional expression $(if\ P\ then\ a\ else\ b)$ and $c$ is equal to $if\ P\ then\ a \cdot c\ else\ b \cdot c$.

dite_mul_dite theorem

 (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) :
  ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Full source

@[to_additive]
lemma dite_mul_dite (a : P → α) (b : ¬ P → α) (c : P → α) (d : ¬ P → α) :
    ((if h : P then a h else b h) * if h : P then c h else d h) =
      if h : P then a h * c h else b h * d h := by split <;> rfl

Multiplication of Dependent If-Then-Else Expressions

Informal description

Let $P$ be a proposition, and let $a, c : P \to \alpha$ and $b, d : \neg P \to \alpha$ be functions. Then the product of the two dependent if-then-else expressions satisfies: \[ \left(\text{if } h : P \text{ then } a(h) \text{ else } b(h)\right) \cdot \left(\text{if } h : P \text{ then } c(h) \text{ else } d(h)\right) = \text{if } h : P \text{ then } a(h) \cdot c(h) \text{ else } b(h) \cdot d(h) \]

ite_mul_ite theorem

(a b c d : α) : ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Full source

@[to_additive]
lemma ite_mul_ite (a b c d : α) :
    ((if P then a else b) * if P then c else d) = if P then a * c else b * d := by split <;> rfl

Conditional Multiplication Identity: $(if\ P\ then\ a\ else\ b) \cdot (if\ P\ then\ c\ else\ d) = if\ P\ then\ a \cdot c\ else\ b \cdot d$

Informal description

For any elements $a, b, c, d$ of type $\alpha$ and any proposition $P$, the product of the conditional expressions $(if\ P\ then\ a\ else\ b)$ and $(if\ P\ then\ c\ else\ d)$ is equal to $if\ P\ then\ a \cdot c\ else\ b \cdot d$.

div_dite theorem

(a : α) (b : P → α) (c : ¬P → α) : (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Full source

@[to_additive]
lemma div_dite (a : α) (b : P → α) (c : ¬ P → α) :
    (a / if h : P then b h else c h) = if h : P then a / b h else a / c h := by split <;> rfl

Division of an Element by a Conditional Expression

Informal description

For any element $a$ in a type $\alpha$ with division, and for any functions $b : P \to \alpha$ and $c : \neg P \to \alpha$, the division of $a$ by a conditional expression (if $h : P$ then $b h$ else $c h$) is equal to the conditional expression (if $h : P$ then $a / b h$ else $a / c h$). In other words: $$ a / \left(\text{if } h : P \text{ then } b h \text{ else } c h\right) = \text{if } h : P \text{ then } a / b h \text{ else } a / c h $$

div_ite theorem

(a b c : α) : (a / if P then b else c) = if P then a / b else a / c

Full source

@[to_additive]
lemma div_ite (a b c : α) : (a / if P then b else c) = if P then a / b else a / c := div_dite ..

Division by Conditional Expression: $a / (\text{if } P \text{ then } b \text{ else } c) = \text{if } P \text{ then } a / b \text{ else } a / c$

Informal description

For any elements $a, b, c$ of a type $\alpha$ with a division operation and any proposition $P$, the division of $a$ by the conditional expression (if $P$ then $b$ else $c$) is equal to the conditional expression (if $P$ then $a / b$ else $a / c$). In other words: $$ a / \left(\text{if } P \text{ then } b \text{ else } c\right) = \text{if } P \text{ then } a / b \text{ else } a / c $$

dite_div theorem

(a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Full source

@[to_additive]
lemma dite_div (a : P → α) (b : ¬ P → α) (c : α) :
    (if h : P then a h else b h) / c = if h : P then a h / c else b h / c := by split <;> rfl

Division of Conditional Expression by Constant

Informal description

Let $\alpha$ be a type with a division operation, and let $P$ be a proposition. For any functions $a : P \to \alpha$, $b : \neg P \to \alpha$, and any element $c : \alpha$, we have \[ \frac{\text{if } h : P \text{ then } a(h) \text{ else } b(h)}{c} = \text{if } h : P \text{ then } \frac{a(h)}{c} \text{ else } \frac{b(h)}{c}. \]

ite_div theorem

(a b c : α) : (if P then a else b) / c = if P then a / c else b / c

Full source

@[to_additive]
lemma ite_div (a b c : α) : (if P then a else b) / c = if P then a / c else b / c := dite_div ..

Division of Conditional Expression: $\frac{\text{if } P \text{ then } a \text{ else } b}{c} = \text{if } P \text{ then } \frac{a}{c} \text{ else } \frac{b}{c}$

Informal description

For any type $\alpha$ with a division operation, given a proposition $P$ and elements $a, b, c \in \alpha$, we have \[ \frac{\text{if } P \text{ then } a \text{ else } b}{c} = \text{if } P \text{ then } \frac{a}{c} \text{ else } \frac{b}{c}. \]

dite_div_dite theorem

 (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) :
  ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Full source

@[to_additive]
lemma dite_div_dite (a : P → α) (b : ¬ P → α) (c : P → α) (d : ¬ P → α) :
    ((if h : P then a h else b h) / if h : P then c h else d h) =
      if h : P then a h / c h else b h / d h := by split <;> rfl

Division of Dependent If-Then-Else Terms

Informal description

For any type $\alpha$ with a division operation, given a proposition $P$ and functions $a, c : P \to \alpha$ and $b, d : \neg P \to \alpha$, the following equality holds: \[ \frac{\text{if } h : P \text{ then } a(h) \text{ else } b(h)}{\text{if } h : P \text{ then } c(h) \text{ else } d(h)} = \text{if } h : P \text{ then } \frac{a(h)}{c(h)} \text{ else } \frac{b(h)}{d(h)} \]

ite_div_ite theorem

(a b c d : α) : ((if P then a else b) / if P then c else d) = if P then a / c else b / d

Full source

@[to_additive]
lemma ite_div_ite (a b c d : α) :
    ((if P then a else b) / if P then c else d) = if P then a / c else b / d := dite_div_dite ..

Division of If-Then-Else Terms: $\frac{\text{if } P \text{ then } a \text{ else } b}{\text{if } P \text{ then } c \text{ else } d} = \text{if } P \text{ then } \frac{a}{c} \text{ else } \frac{b}{d}$

Informal description

For any type $\alpha$ with a division operation and any proposition $P$, given four elements $a, b, c, d \in \alpha$, the following equality holds: \[ \frac{\text{if } P \text{ then } a \text{ else } b}{\text{if } P \text{ then } c \text{ else } d} = \text{if } P \text{ then } \frac{a}{c} \text{ else } \frac{b}{d} \]

One structure

(α : Type u)

Full source

@[to_additive]
class One (α : Type u) where
  one : α

Multiplicative Identity

Informal description

The structure representing the multiplicative identity element in a type `α`.

One.toOfNat1 instance

{α} [One α] : OfNat α (nat_lit 1)

Full source

@[to_additive existing Zero.toOfNat0]
instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

Canonical Interpretation of 1 in Types with One

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, there is a canonical way to interpret the numeral `1` as an element of $\alpha$.

One.ofOfNat1 instance

{α} [OfNat α (nat_lit 1)] : One α

Full source

@[to_additive existing Zero.ofOfNat0, to_additive_change_numeral 2]
instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

Canonical Multiplicative Identity from Numeric Literal 1

Informal description

For any type $\alpha$ with a distinguished element `1` (interpreted via the `OfNat` typeclass), there is a canonical multiplicative identity structure on $\alpha$.

Zero.instNonempty instance

[Zero α] : Nonempty α

Full source

instance (priority := 20) Zero.instNonempty [Zero α] : Nonempty α := ⟨0⟩

Nonemptiness of Types with Zero

Informal description

For any type $\alpha$ with a zero element, $\alpha$ is nonempty.

One.instNonempty instance

[One α] : Nonempty α

Full source

instance (priority := 20) One.instNonempty [One α] : Nonempty α := ⟨1⟩

Nonemptiness of Types with One

Informal description

For any type $\alpha$ with a multiplicative identity element, $\alpha$ is nonempty.