class One₁ (α : Type) : Type

• one : α

  The element one

class One₂ (α : Type) : Type

• one : α

  The element one

def «term𝟙» : Lean.ParserDescr

The element one

Equations

• «term𝟙» = Lean.ParserDescr.node `term𝟙 1024 (Lean.ParserDescr.symbol "𝟙")

class Dia₁ (α : Type) : Type

• dia : α → α → α

def «term_⋄_» : Lean.TrailingParserDescr

Equations

• «term_⋄_» = Lean.ParserDescr.trailingNode `term_⋄_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋄ ") (Lean.ParserDescr.cat `term 71))

class Semigroup₁ (α : Type) : Type

• toDia₁ : Dia₁ α
• dia_assoc : ∀ (a b c : α), a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

  Diamond is associative

theorem Semigroup₁.dia_assoc {α : Type} [self : Semigroup₁ α] (a : α) (b : α) (c : α) : a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Diamond is associative

class Semigroup₂ (α : Type) extends Dia₁ : Type

• dia : α → α → α
• dia_assoc : ∀ (a b c : α), a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

  Diamond is associative

theorem Semigroup₂.dia_assoc {α : Type} [self : Semigroup₂ α] (a : α) (b : α) (c : α) : a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Diamond is associative

class DiaOneClass₁ (α : Type) extends One₁ , Dia₁ : Type

• one : α
• dia : α → α → α
• one_dia : ∀ (a : α), 𝟙 ⋄ a = a

  One is a left neutral element for diamond.

• dia_one : ∀ (a : α), a ⋄ 𝟙 = a

  One is a right neutral element for diamond

theorem DiaOneClass₁.one_dia {α : Type} [self : DiaOneClass₁ α] (a : α) : 𝟙 ⋄ a = a

One is a left neutral element for diamond.

theorem DiaOneClass₁.dia_one {α : Type} [self : DiaOneClass₁ α] (a : α) : a ⋄ 𝟙 = a

One is a right neutral element for diamond

class Monoid₁ (α : Type) extends Semigroup₁ , One₁ : Type

• toDia₁ : Dia₁ α
• dia_assoc : ∀ (a b c : α), a ⋄ b ⋄ c = a ⋄ (b ⋄ c)
• one : α
• one_dia : ∀ (a : α), 𝟙 ⋄ a = a

  One is a left neutral element for diamond.

• dia_one : ∀ (a : α), a ⋄ 𝟙 = a

  One is a right neutral element for diamond

class Monoid₂ (α : Type) : Type

• toSemigroup₁ : Semigroup₁ α
• toDiaOneClass₁ : DiaOneClass₁ α

class Inv₁ (α : Type) : Type

• inv : α → α

  The inversion function

def «term_⁻¹_1» : Lean.TrailingParserDescr

The inversion function

Equations

• «term_⁻¹_1» = Lean.ParserDescr.trailingNode `term_⁻¹_1 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

class Group₁ (G : Type) extends Monoid₁ , Inv₁ : Type

• toDia₁ : Dia₁ G
• dia_assoc : ∀ (a b c : G), a ⋄ b ⋄ c = a ⋄ (b ⋄ c)
• one : G
• one_dia : ∀ (a : G), 𝟙 ⋄ a = a
• dia_one : ∀ (a : G), a ⋄ 𝟙 = a
• inv : G → G
• inv_dia : ∀ (a : G), a⁻¹ ⋄ a = 𝟙

theorem Group₁.inv_dia {G : Type} [self : Group₁ G] (a : G) : a⁻¹ ⋄ a = 𝟙

theorem left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a : M} {b : M} {c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c

theorem inv_eq_of_dia {G : Type} [Group₁ G] {a : G} {b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b

theorem dia_inv {G : Type} [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙

class AddSemigroup₃ (α : Type) extends Add : Type

• add : α → α → α
• add_assoc₃ : ∀ (a b c : α), a + b + c = a + (b + c)

  Addition is associative

theorem AddSemigroup₃.add_assoc₃ {α : Type} [self : AddSemigroup₃ α] (a : α) (b : α) (c : α) : a + b + c = a + (b + c)

Addition is associative

class Semigroup₃ (α : Type) extends Mul : Type

• mul : α → α → α
• mul_assoc₃ : ∀ (a b c : α), a * b * c = a * (b * c)

  Multiplication is associative

theorem Semigroup₃.mul_assoc₃ {α : Type} [self : Semigroup₃ α] (a : α) (b : α) (c : α) : a * b * c = a * (b * c)

Multiplication is associative

class AddMonoid₃ (α : Type) extends AddSemigroup₃ , Zero : Type

• add : α → α → α
• add_assoc₃ : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : α), a + 0 = a

  Zero is a right neutral element for addition

class Monoid₃ (α : Type) extends Semigroup₃ , One : Type

• mul : α → α → α
• mul_assoc₃ : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a

  One is a left neutral element for multiplication

• mul_one : ∀ (a : α), a * 1 = a

  One is a right neutral element for multiplication

theorem left_neg_eq_right_neg' {M : Type} [AddMonoid₃ M] {a : M} {b : M} {c : M} (hba : b + a = 0) (hac : a + c = 0) : b = c

theorem left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a : M} {b : M} {c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ : Type

• add : α → α → α
• add_assoc₃ : ∀ (a b c : α), a + b + c = a + (b + c)
• add_comm : ∀ (a b : α), a + b = b + a

theorem AddCommSemigroup₃.add_comm {α : Type} [self : AddCommSemigroup₃ α] (a : α) (b : α) : a + b = b + a

class CommSemigroup₃ (α : Type) extends Semigroup₃ : Type

• mul : α → α → α
• mul_assoc₃ : ∀ (a b c : α), a * b * c = a * (b * c)
• mul_comm : ∀ (a b : α), a * b = b * a

theorem CommSemigroup₃.mul_comm {α : Type} [self : CommSemigroup₃ α] (a : α) (b : α) : a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ : Type

• add : α → α → α
• add_assoc₃ : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• add_comm : ∀ (a b : α), a + b = b + a

class CommMonoid₃ (α : Type) extends Monoid₃ : Type

• mul : α → α → α
• mul_assoc₃ : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• mul_comm : ∀ (a b : α), a * b = b * a

class AddGroup₃ (G : Type) extends AddMonoid₃ , Neg : Type

• add : G → G → G
• add_assoc₃ : ∀ (a b c : G), a + b + c = a + (b + c)
• zero : G
• zero_add : ∀ (a : G), 0 + a = a
• add_zero : ∀ (a : G), a + 0 = a
• neg : G → G
• neg_add : ∀ (a : G), -a + a = 0

@[simp]

theorem AddGroup₃.neg_add {G : Type} [self : AddGroup₃ G] (a : G) : -a + a = 0

class Group₃ (G : Type) extends Monoid₃ , Inv : Type

• mul : G → G → G
• mul_assoc₃ : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• inv : G → G
• inv_mul : ∀ (a : G), a⁻¹ * a = 1

@[simp]

theorem Group₃.inv_mul {G : Type} [self : Group₃ G] (a : G) : a⁻¹ * a = 1

theorem neg_eq_of_add {G : Type} [AddGroup₃ G] {a : G} {b : G} (h : a + b = 0) : -a = b

theorem inv_eq_of_mul {G : Type} [Group₃ G] {a : G} {b : G} (h : a * b = 1) : a⁻¹ = b

@[simp]

theorem AddGroup₃.add_neg {G : Type} [AddGroup₃ G] {a : G} : a + -a = 0

@[simp]

theorem Group₃.mul_inv {G : Type} [Group₃ G] {a : G} : a * a⁻¹ = 1

theorem add_left_cancel₃ {G : Type} [AddGroup₃ G] {a : G} {b : G} {c : G} (h : a + b = a + c) : b = c

theorem mul_left_cancel₃ {G : Type} [Group₃ G] {a : G} {b : G} {c : G} (h : a * b = a * c) : b = c

theorem add_right_cancel₃ {G : Type} [AddGroup₃ G] {a : G} {b : G} {c : G} (h : b + a = c + a) : b = c

theorem mul_right_cancel₃ {G : Type} [Group₃ G] {a : G} {b : G} {c : G} (h : b * a = c * a) : b = c

class AddCommGroup₃ (G : Type) extends AddGroup₃ : Type

• add : G → G → G
• add_assoc₃ : ∀ (a b c : G), a + b + c = a + (b + c)
• zero : G
• zero_add : ∀ (a : G), 0 + a = a
• add_zero : ∀ (a : G), a + 0 = a
• neg : G → G
• neg_add : ∀ (a : G), -a + a = 0
• add_comm : ∀ (a b : G), a + b = b + a

class CommGroup₃ (G : Type) extends Group₃ : Type

• mul : G → G → G
• mul_assoc₃ : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• inv : G → G
• inv_mul : ∀ (a : G), a⁻¹ * a = 1
• mul_comm : ∀ (a b : G), a * b = b * a

class Ring₃ (R : Type) extends AddGroup₃ , Monoid₃ : Type

• add : R → R → R
• add_assoc₃ : ∀ (a b c : R), a + b + c = a + (b + c)
• zero : R
• zero_add : ∀ (a : R), 0 + a = a
• add_zero : ∀ (a : R), a + 0 = a
• neg : R → R
• neg_add : ∀ (a : R), -a + a = 0
• mul : R → R → R
• mul_assoc₃ : ∀ (a b c : R), a * b * c = a * (b * c)
• one : R
• one_mul : ∀ (a : R), 1 * a = a
• mul_one : ∀ (a : R), a * 1 = a
• zero_mul : ∀ (a : R), 0 * a = 0

  Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : R), a * 0 = 0

  Zero is a right absorbing element for multiplication

• left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c

  Multiplication is left distributive over addition

• right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c

  Multiplication is right distributive over addition

theorem Ring₃.left_distrib {R : Type} [self : Ring₃ R] (a : R) (b : R) (c : R) : a * (b + c) = a * b + a * c

Multiplication is left distributive over addition

theorem Ring₃.right_distrib {R : Type} [self : Ring₃ R] (a : R) (b : R) (c : R) : (a + b) * c = a * c + b * c

Multiplication is right distributive over addition

instance instAddCommGroup₃OfRing₃ {R : Type} [Ring₃ R] : AddCommGroup₃ R

Equations

• instAddCommGroup₃OfRing₃ = AddCommGroup₃.mk ⋯

instance instRing₃Int : Ring₃ ℤ

Equations

• instRing₃Int = Ring₃.mk instRing₃Int.proof_6 instRing₃Int.proof_7 Int.mul_add Int.add_mul

class LE₁ (α : Type) : Type

• le : α → α → Prop

  The Less-or-Equal relation.

def «term_≤₁_» : Lean.TrailingParserDescr

The Less-or-Equal relation.

Equations

• «term_≤₁_» = Lean.ParserDescr.trailingNode `term_≤₁_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤₁ ") (Lean.ParserDescr.cat `term 51))

class Preorder₁ (α : Type) : Type

class PartialOrder₁ (α : Type) : Type

class OrderedCommMonoid₁ (α : Type) : Type

instance instOrderedCommMonoid₁Nat : OrderedCommMonoid₁ ℕ

Equations

• instOrderedCommMonoid₁Nat = { }

class SMul₃ (α : Type) (β : Type) : Type

• smul : α → β → β

  Scalar multiplication

def «term_•__1» : Lean.TrailingParserDescr

Equations

• «term_•__1» = Lean.ParserDescr.trailingNode `term_•__1 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 73))

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ : Type

• smul : R → M → M
• zero_smul : ∀ (m : M), 0 • m = 0
• one_smul : ∀ (m : M), 1 • m = m
• mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
• add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
• smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

theorem Module₁.zero_smul {R : Type} : ∀ {inst : Ring₃ R} {M : Type} {inst_1 : AddCommGroup₃ M} [self : Module₁ R M] (m : M), 0 • m = 0

theorem Module₁.one_smul {R : Type} : ∀ {inst : Ring₃ R} {M : Type} {inst_1 : AddCommGroup₃ M} [self : Module₁ R M] (m : M), 1 • m = m

theorem Module₁.mul_smul {R : Type} : ∀ {inst : Ring₃ R} {M : Type} {inst_1 : AddCommGroup₃ M} [self : Module₁ R M] (a b : R) (m : M), (a * b) • m = a • b • m

theorem Module₁.add_smul {R : Type} : ∀ {inst : Ring₃ R} {M : Type} {inst_1 : AddCommGroup₃ M} [self : Module₁ R M] (a b : R) (m : M), (a + b) • m = a • m + b • m

theorem Module₁.smul_add {R : Type} : ∀ {inst : Ring₃ R} {M : Type} {inst_1 : AddCommGroup₃ M} [self : Module₁ R M] (a : R) (m n : M), a • (m + n) = a • m + a • n

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R

Equations

• selfModule R = Module₁.mk ⋯ ⋯ ⋯ ⋯ ⋯

def nsmul₁ {M : Type u_1} [Zero M] [Add M] : ℕ → M → M

Equations

• nsmul₁ 0 x = 0
• nsmul₁ n.succ x = x + nsmul₁ n x

def zsmul₁ {M : Type u_1} [Zero M] [Add M] [Neg M] : ℤ → M → M

Equations

• zsmul₁ (Int.ofNat n) x = nsmul₁ n x
• zsmul₁ (Int.negSucc n) x = -nsmul₁ n.succ x

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A

Equations

• abGrpModule A = Module₁.mk ⋯ ⋯ ⋯ ⋯ ⋯

class AddMonoid₄ (M : Type) extends AddSemigroup₃ , Zero : Type

• add : M → M → M
• add_assoc₃ : ∀ (a b c : M), a + b + c = a + (b + c)
• zero : M
• zero_add : ∀ (a : M), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : M), a + 0 = a

  Zero is a right neutral element for addition

• nsmul : ℕ → M → M

  Multiplication by a natural number.

• nsmul_zero : ∀ (x : M), AddMonoid₄.nsmul 0 x = 0

  Multiplication by (0 : ℕ) gives 0.

• nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid₄.nsmul (n + 1) x = x + AddMonoid₄.nsmul n x

  Multiplication by (n + 1 : ℕ) behaves as expected.

theorem AddMonoid₄.nsmul_zero {M : Type} [self : AddMonoid₄ M] (x : M) : AddMonoid₄.nsmul 0 x = 0

Multiplication by (0 : ℕ) gives 0.

theorem AddMonoid₄.nsmul_succ {M : Type} [self : AddMonoid₄ M] (n : ℕ) (x : M) : AddMonoid₄.nsmul (n + 1) x = x + AddMonoid₄.nsmul n x

Multiplication by (n + 1 : ℕ) behaves as expected.

instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M

Equations

• mySMul = { smul := AddMonoid₄.nsmul }

instance instAddMonoid₄Prod (M : Type) (N : Type) [AddMonoid₄ M] [AddMonoid₄ N] : AddMonoid₄ (M × N)

Equations

• instAddMonoid₄Prod M N = AddMonoid₄.mk ⋯ ⋯ nsmul₁ ⋯ ⋯

instance instAddMonoid₄Int : AddMonoid₄ ℤ

Equations

• instAddMonoid₄Int = AddMonoid₄.mk Int.zero_add Int.add_zero (fun (n : ℕ) (m : ℤ) => ↑n * m) Int.zero_mul instAddMonoid₄Int.proof_1