# 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.

We introduce the notation typeclass `Star` for algebraic structures with a star operation. Note: to accommodate diverse notational preferences, no default notation is provided for `Star.star`.

`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`.

source
class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

The notation typeclass for heterogeneous additive actions. This enables the notation `a +ᵥ b : γ` where `a : α`, `b : β`.

- hVAdd : α → β → γ

  `a +ᵥ b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent.

Instances

source
class VAdd (G : Type u) (P : Type v) :
Type (max u v)

Type class for the `+ᵥ` notation.

- vadd : G → P → P

  `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.

Instances

source
class VSub (G : outParam (Type u_1)) (P : Type u_2) :
Type (max u_1 u_2)

Type class for the `-ᵥ` notation.

- vsub : P → P → G

  `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.

Instances

source
theorem SMul.ext_iff {M : Type u} {α : Type v} {x y : SMul M α} :
x = y ↔ smul = smul
source
theorem VAdd.ext_iff {G : Type u} {P : Type v} {x y : VAdd G P} :
x = y ↔ vadd = vadd
source
theorem VAdd.ext {G : Type u} {P : Type v} {x y : VAdd G P} (vadd : vadd = vadd) :
x = y
source
theorem SMul.ext {M : Type u} {α : Type v} {x y : SMul M α} (smul : smul = smul) :
x = y
source
def «term_+ᵥ_» :
Lean.TrailingParserDescr

`a +ᵥ b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent.

Equations

- «term_+ᵥ_» = Lean.ParserDescr.trailingNode `«term_+ᵥ_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ ") (Lean.ParserDescr.cat `term 65))

Instances For

source
def «term_-ᵥ_» :
Lean.TrailingParserDescr

`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.

Equations

- «term_-ᵥ_» = Lean.ParserDescr.trailingNode `«term_-ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ᵥ ") (Lean.ParserDescr.cat `term 66))

Instances For

source
@[defaultInstance 1000]
instance instHVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] :
HVAdd α β β
Equations

- instHVAdd = { hVAdd := VAdd.vadd }

source
class Star (R : Type u) :
Type u

Notation typeclass (with no default notation!) for an algebraic structure with a star operation.

- star : R → R

  A star operation (e.g. complex conjugate).

Instances

source
@[simp]
theorem mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (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
source
theorem add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (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
source
@[simp]
theorem mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c : α) :
(a * if P then b else c) = if P then a * b else a * c
source
theorem add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c : α) :
(a + if P then b else c) = if P then a + b else a + c
source
@[simp]
theorem dite_mul {α : Type u_2} (P : Prop) [Decidable P] [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
source
theorem dite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (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
source
@[simp]
theorem ite_mul {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c : α) :
(if P then a else b) * c = if P then a * c else b * c
source
theorem ite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c : α) :
(if P then a else b) + c = if P then a + c else b + c
source
theorem dite_mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (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
source
theorem dite_add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (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
source
theorem ite_mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c d : α) :
((if P then a else b) * if P then c else d) = if P then a * c else b * d
source
theorem ite_add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c d : α) :
((if P then a else b) + if P then c else d) = if P then a + c else b + d
source
theorem div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (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
source
theorem sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (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
source
theorem div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c : α) :
(a / if P then b else c) = if P then a / b else a / c
source
theorem sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c : α) :
(a - if P then b else c) = if P then a - b else a - c
source
theorem dite_div {α : Type u_2} (P : Prop) [Decidable P] [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
source
theorem dite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (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
source
theorem ite_div {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c : α) :
(if P then a else b) / c = if P then a / c else b / c
source
theorem ite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c : α) :
(if P then a else b) - c = if P then a - c else b - c
source
theorem dite_div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (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
source
theorem dite_sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (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
source
theorem ite_div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c d : α) :
((if P then a else b) / if P then c else d) = if P then a / c else b / d
source
theorem ite_sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c d : α) :
((if P then a else b) - if P then c else d) = if P then a - c else b - d
source
@[instance 20]
instance Zero.instNonempty {α : Type u} [Zero α] :
Nonempty α
source
@[instance 20]
instance One.instNonempty {α : Type u} [One α] :
Nonempty α
source
theorem Subsingleton.eq_one {α : Type u} [One α] [Subsingleton α] (a : α) :
a = 1
source
theorem Subsingleton.eq_zero {α : Type u} [Zero α] [Subsingleton α] (a : α) :
a = 0