mathlib documentation

core / init.algebra.classes

Unbundled algebra classes #

These classes and the @[algebra] attribute are part of an incomplete refactor described here on the github Wiki.

By themselves, these classes are not good replacements for the monoid / group etc structures provided by mathlib, as they are not discoverable by simp unlike the current lemmas due to there being little to index on. The Wiki page linked above describes an algebraic normalizer, but it is not implemented.

@[class]
structure is_symm_op (α : Type u) (β : out_param (Type v)) (op : α → α → β) :
Prop
  • symm_op : ∀ (a b : α), op a b = op b a
Instances of this typeclass
@[protected, instance]
def is_symm_op_of_is_commutative (α : Type u) (op : α → α → α) [is_commutative α op] :
is_symm_op α α op
@[class]
structure is_left_id (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • left_id : ∀ (a : α), op o a = a
Instances of this typeclass
@[class]
structure is_right_id (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • right_id : ∀ (a : α), op a o = a
Instances of this typeclass
@[class]
structure is_left_null (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • left_null : ∀ (a : α), op o a = o
@[class]
structure is_right_null (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • right_null : ∀ (a : α), op a o = o
@[class]
structure is_left_cancel (α : Type u) (op : α → α → α) :
Prop
  • left_cancel : ∀ (a b c : α), op a b = op a cb = c
Instances of this typeclass
@[class]
structure is_right_cancel (α : Type u) (op : α → α → α) :
Prop
  • right_cancel : ∀ (a b c : α), op a b = op c ba = c
Instances of this typeclass
@[class]
structure is_idempotent (α : Type u) (op : α → α → α) :
Prop
  • idempotent : ∀ (a : α), op a a = a
Instances of this typeclass
@[class]
structure is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param (α → α → α)) :
Prop
  • left_distrib : ∀ (a b c : α), op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)
@[class]
structure is_right_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param (α → α → α)) :
Prop
  • right_distrib : ∀ (a b c : α), op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)
@[class]
structure is_left_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :
Prop
  • left_inv : ∀ (a : α), op (inv a) a = o
@[class]
structure is_right_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :
Prop
  • right_inv : ∀ (a : α), op a (inv a) = o
@[class]
structure is_cond_left_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) (p : out_param (α → Prop)) :
Prop
  • left_inv : ∀ (a : α), p aop (inv a) a = o
@[class]
structure is_cond_right_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) (p : out_param (α → Prop)) :
Prop
  • right_inv : ∀ (a : α), p aop a (inv a) = o
@[class]
structure is_distinct (α : Type u) (a b : α) :
Prop
  • distinct : a b
@[class]
structure is_symm (α : Type u) (r : α → α → Prop) :
Prop
  • symm : ∀ (a b : α), r a br b a

is_symm X r means the binary relation r on X is symmetric.

Instances of this typeclass
@[protected, instance]
def is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm α r] :
is_symm_op α Prop r

The opposite of a symmetric relation is symmetric.

@[class]
structure is_asymm (α : Type u) (r : α → α → Prop) :
Prop
  • asymm : ∀ (a b : α), r a b¬r b a

is_asymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

Instances of this typeclass
@[class]
structure is_total (α : Type u) (r : α → α → Prop) :
Prop
  • total : ∀ (a b : α), r a b r b a

is_total X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

Instances of this typeclass
@[class]
structure is_preorder (α : Type u) (r : α → α → Prop) :
Prop

is_preorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

Instances of this typeclass
@[class]
structure is_total_preorder (α : Type u) (r : α → α → Prop) :
Prop

is_total_preorder X r means that the binary relation r on X is total and a preorder.

Instances of this typeclass
@[protected, instance]
def is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] :

Every total pre-order is a pre-order.

@[class]
structure is_partial_order (α : Type u) (r : α → α → Prop) :
Prop

is_partial_order X r means that the binary relation r on X is a partial order, that is, is_preorder X r and is_antisymm X r.

Instances of this typeclass
@[class]
structure is_linear_order (α : Type u) (r : α → α → Prop) :
Prop

is_linear_order X r means that the binary relation r on X is a linear order, that is, is_partial_order X r and is_total X r.

Instances of this typeclass
@[class]
structure is_equiv (α : Type u) (r : α → α → Prop) :
Prop

is_equiv X r means that the binary relation r on X is an equivalence relation, that is, is_preorder X r and is_symm X r.

Instances of this typeclass
@[class]
structure is_per (α : Type u) (r : α → α → Prop) :
Prop

is_per X r means that the binary relation r on X is a partial equivalence relation, that is, is_symm X r and is_trans X r.

@[class]
structure is_strict_order (α : Type u) (r : α → α → Prop) :
Prop

is_strict_order X r means that the binary relation r on X is a strict order, that is, is_irrefl X r and is_trans X r.

Instances of this typeclass
@[class]
structure is_incomp_trans (α : Type u) (lt : α → α → Prop) :
Prop
  • incomp_trans : ∀ (a b c : α), ¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a

is_incomp_trans X lt means that for lt a binary relation on X, the incomparable relation λ a b, ¬ lt a b ∧ ¬ lt b a is transitive.

Instances of this typeclass
@[class]
structure is_strict_weak_order (α : Type u) (lt : α → α → Prop) :
Prop

is_strict_weak_order X lt means that the binary relation lt on X is a strict weak order, that is, is_strict_order X lt and is_incomp_trans X lt.

Instances of this typeclass
@[class]
structure is_strict_total_order (α : Type u) (lt : α → α → Prop) :
Prop

is_strict_total_order X lt means that the binary relation lt on X is a strict total order, that is, is_trichotomous X lt and is_strict_order X lt.

Instances of this typeclass
@[protected, instance]
def eq_is_equiv (α : Type u) :

Equality is an equivalence relation.

theorem irrefl {α : Type u} {r : α → α → Prop} [is_irrefl α r] (a : α) :
¬r a a
theorem refl {α : Type u} {r : α → α → Prop} [is_refl α r] (a : α) :
r a a
theorem trans {α : Type u} {r : α → α → Prop} [is_trans α r] {a b c : α} :
r a br b cr a c
theorem symm {α : Type u} {r : α → α → Prop} [is_symm α r] {a b : α} :
r a br b a
theorem antisymm {α : Type u} {r : α → α → Prop} [is_antisymm α r] {a b : α} :
r a br b aa = b
theorem asymm {α : Type u} {r : α → α → Prop} [is_asymm α r] {a b : α} :
r a b¬r b a
theorem trichotomous {α : Type u} {r : α → α → Prop} [is_trichotomous α r] (a b : α) :
r a b a = b r b a
theorem incomp_trans {α : Type u} {r : α → α → Prop} [is_incomp_trans α r] {a b c : α} :
¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
@[protected, instance]
def is_asymm_of_is_trans_of_is_irrefl {α : Type u} {r : α → α → Prop} [is_trans α r] [is_irrefl α r] :
theorem irrefl_of {α : Type u} (r : α → α → Prop) [is_irrefl α r] (a : α) :
¬r a a
theorem refl_of {α : Type u} (r : α → α → Prop) [is_refl α r] (a : α) :
r a a
theorem trans_of {α : Type u} (r : α → α → Prop) [is_trans α r] {a b c : α} :
r a br b cr a c
theorem symm_of {α : Type u} (r : α → α → Prop) [is_symm α r] {a b : α} :
r a br b a
theorem asymm_of {α : Type u} (r : α → α → Prop) [is_asymm α r] {a b : α} :
r a b¬r b a
theorem total_of {α : Type u} (r : α → α → Prop) [is_total α r] (a b : α) :
r a b r b a
theorem trichotomous_of {α : Type u} (r : α → α → Prop) [is_trichotomous α r] (a b : α) :
r a b a = b r b a
theorem incomp_trans_of {α : Type u} (r : α → α → Prop) [is_incomp_trans α r] {a b c : α} :
¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
def strict_weak_order.equiv {α : Type u} {r : α → α → Prop} (a b : α) :
Prop
Equations
Instances for strict_weak_order.equiv
theorem strict_weak_order.erefl {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] (a : α) :
theorem strict_weak_order.esymm {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :
theorem strict_weak_order.etrans {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b c : α} :
theorem strict_weak_order.not_lt_of_equiv {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :
theorem strict_weak_order.not_lt_of_equiv' {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :
@[protected, instance]
def strict_weak_order.is_equiv {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] :
theorem is_strict_weak_order_of_is_total_preorder {α : Type u} {le lt : α → α → Prop} [decidable_rel le] [s : is_total_preorder α le] (h : ∀ (a b : α), lt a b ¬le b a) :
theorem lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] {a b c : α} :
lt a b¬lt b c ¬lt c blt a c
theorem lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] {a b c : α} :
¬lt a b ¬lt b alt b clt a c
theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :
¬lt a b ¬lt b aa = b
theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :
theorem incomp_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b : α) :
¬lt a b ¬lt b a a = b
theorem eqv_lt_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b : α) :
theorem not_lt_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_order α lt] {a b : α} :
lt a b¬lt b a