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.

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.

  Conventions for notations in identifiers:

  • The recommended spelling of +ᵥ in identifiers is vadd.

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.

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.

  Conventions for notations in identifiers:

  • The recommended spelling of -ᵥ in identifiers is vsub.

theorem SMul.ext_iff {M : Type u} {α : Type v} {x y : SMul M α} : x = y ↔ smul = smul

theorem VAdd.ext_iff {G : Type u} {P : Type v} {x y : VAdd G P} : x = y ↔ vadd = vadd

theorem VAdd.ext {G : Type u} {P : Type v} {x y : VAdd G P} (vadd : vadd = vadd) : x = y

theorem SMul.ext {M : Type u} {α : Type v} {x y : SMul M α} (smul : smul = smul) : x = y

def «term_+ᵥ_» : Lean.TrailingParserDescr

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

Conventions for notations in identifiers:

• The recommended spelling of +ᵥ in identifiers is vadd.

Equations

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

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.

Conventions for notations in identifiers:

• The recommended spelling of -ᵥ in identifiers is vsub.

Equations

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

@[defaultInstance 1000]

instance instHVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] : HVAdd α β β

Equations

• instHVAdd = { hVAdd := VAdd.vadd }

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

@[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

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

@[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

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

@[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

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

@[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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[instance 20]

instance One.instNonempty {α : Type u} [One α] : Nonempty α

@[instance 20]

instance Zero.instNonempty {α : Type u} [Zero α] : Nonempty α

theorem Subsingleton.eq_one {α : Type u} [One α] [Subsingleton α] (a : α) : a = 1

theorem Subsingleton.eq_zero {α : Type u} [Zero α] [Subsingleton α] (a : α) : a = 0