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
@[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
@[class]
structure is_right_id (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • right_id : ∀ (a : α), op a o = a
Instances
@[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
@[class]
structure is_right_cancel (α : Type u) (op : α → α → α) :
Prop
  • right_cancel : ∀ (a b c : α), op a b = op c ba = c
Instances
@[class]
structure is_idempotent (α : Type u) (op : α → α → α) :
Prop
  • idempotent : ∀ (a : α), op a a = a
Instances
@[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_irrefl (α : Type u) (r : α → α → Prop) :
Prop
  • irrefl : ∀ (a : α), ¬r a a

is_irrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

Instances
@[class]
structure is_refl (α : Type u) (r : α → α → Prop) :
Prop
  • refl : ∀ (a : α), r a a

is_refl X r means the binary relation r on X is reflexive.

Instances
@[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
@[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
@[class]
structure is_antisymm (α : Type u) (r : α → α → Prop) :
Prop
  • antisymm : ∀ (a b : α), r a br b aa = b

is_antisymm X r means the binary relation r on X is antisymmetric.

Instances
@[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
@[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
@[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
@[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
Instances
@[class]
structure is_linear_order (α : Type u) (r : α → α → Prop) :
Prop
Instances
@[class]
structure is_equiv (α : Type u) (r : α → α → Prop) :
Prop
Instances
@[class]
structure is_per (α : Type u) (r : α → α → Prop) :
Prop
@[class]
structure is_strict_order (α : Type u) (r : α → α → Prop) :
Prop
Instances
@[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
Instances
@[class]
structure is_strict_weak_order (α : Type u) (lt : α → α → Prop) :
Prop
Instances
@[class]
structure is_strict_total_order (α : Type u) (lt : α → α → Prop) :
Prop
Instances
@[protected, instance]
def eq_is_equiv (α : Type u) :
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
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