# Documentation

Mathlib.Init.Algebra.Classes

# Unbundled algebra classes #

These classes are part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

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.

## Porting notes: #

This file is ancient, and it would be good to replace it with a clean version that provides what mathlib4 actually needs.

I've omitted all the @[algebra] attributes, as they are not used elsewhere.

The section StrictWeakOrder has been omitted, but I've left the mathport output in place. Please delete if cleaning up.

I've commented out some classes which we think are completely unused in mathlib.

I've added many of the declarations to nolints.json. If you clean up this file, please add documentation to classes that we are keeping.

Mario made the following analysis of uses in mathlib3:

• is_symm_op: unused except for some instances
• is_commutative: used a fair amount via some theorems about folds (also assuming is_associative)
• is_associative: ditto, also used in noncomm_fold
• is_left_id, is_right_id: unused except in the mathlib class is_unital and in mono (which looks like it could use is_unital)
• is_left_null, is_right_null: unused
• is_left_cancel, is_right_cancel: unused except for instances
• is_idempotent: this one is actually used to prove things not directly about is_idempotent
• is_left_distrib, is_right_distrib, is_left_inv, is_right_inv, is_cond_left_inv, is_cond_right_inv: unused
• is_distinct: unused (although we reinvented this one as nontrivial)
• is_irrefl, is_refl, is_symm, is_trans: significant usage
• is_asymm, is_antisymm, is_total, is_strict_order: a lot of uses but all in order theory and it's unclear how much could not be transferred to another typeclass
• is_preorder: unused except for instances (except antisymmetrization, maybe it could be transferred)
• is_total_preorder, is_partial_order: unused except for instances
• is_linear_order: unused except for instances
• is_equiv: unused except for instances (most uses can use equivalence instead)
• is_per: unused
• is_incomp_trans: unused
• is_strict_weak_order: significant usage (most of it on rbmap, could be transferred)
• is_trichotomous: some usage
• is_strict_total_order: looks like the only usage is in rbmap again
class IsSymmOp (α : Type u) (β : Type v) (op : ααβ) :
• symm_op : ∀ (a b : α), op a b = op b a
Instances
class IsCommutative (α : Type u) (op : ααα) :
• comm : ∀ (a b : α), op a b = op b a

A commutative binary operation.

Instances
instance instIsCommutative {α : Type u_1} {op : ααα} [inst : ] :
Equations
• instIsCommutative = { comm := (_ : ∀ (a b : α), op a b = op b a) }
instance isSymmOp_of_isCommutative (α : Type u) (op : ααα) [inst : ] :
IsSymmOp α α op
Equations
class IsAssociative (α : Type u) (op : ααα) :
• assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

An associative binary operation.

Instances
instance instIsAssociative {α : Type u_1} {op : ααα} [inst : ] :
Equations
• instIsAssociative = { assoc := (_ : ∀ (a b c : α), op (op a b) c = op a (op b c)) }
class IsLeftId (α : Type u) (op : ααα) (o : ) :
• left_id : ∀ (a : α), op o a = a

A binary operation with a left identity.

Instances
class IsRightId (α : Type u) (op : ααα) (o : ) :
• right_id : ∀ (a : α), op a o = a

A binary operation with a right identity.

Instances
instance instIsNeutral {α : Type u_1} {op : ααα} {o : α} [inst : IsLeftId α op o] [inst : IsRightId α op o] :
Equations
• instIsNeutral = { left_neutral := (_ : ∀ (a : α), op o a = a), right_neutral := (_ : ∀ (a : α), op a o = a) }
class IsLeftCancel (α : Type u) (op : ααα) :
• left_cancel : ∀ (a b c : α), op a b = op a cb = c
Instances
class IsRightCancel (α : Type u) (op : ααα) :
• right_cancel : ∀ (a b c : α), op a b = op c ba = c
Instances
class IsIdempotent (α : Type u) (op : ααα) :
• idempotent : ∀ (a : α), op a a = a
Instances
instance instIsIdempotent {α : Type u_1} {op : ααα} [inst : IsIdempotent α op] :
Equations
• instIsIdempotent = { idempotent := (_ : ∀ (a : α), op a a = a) }
class IsIrrefl (α : Type u) (r : ααProp) :
• irrefl : ∀ (a : α), ¬r a a

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

Instances
class IsRefl (α : Type u) (r : ααProp) :
• refl : (a : α) → r a a

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

Instances
class IsSymm (α : Type u) (r : ααProp) :
• symm : (a b : α) → r a br b a

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

Instances
instance isSymmOp_of_isSymm (α : Type u) (r : ααProp) [inst : IsSymm α r] :

The opposite of a symmetric relation is symmetric.

Equations
class IsAsymm (α : Type u) (r : ααProp) :
• asymm : ∀ (a b : α), r a b¬r b a

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

Instances
class IsAntisymm (α : Type u) (r : ααProp) :
• antisymm : ∀ (a b : α), r a br b aa = b

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

Instances
class IsTrans (α : Type u) (r : ααProp) :
• trans : (a b c : α) → r a br b cr a c

IsTrans X r means the binary relation r on X is transitive.

Instances
instance instTrans {α : Type u} {r : ααProp} [inst : IsTrans α r] :
Trans r r r
Equations
instance instIsTrans {α : Type u} {r : ααProp} [inst : Trans r r r] :
IsTrans α r
Equations
class IsTotal (α : Type u) (r : ααProp) :
• total : ∀ (a b : α), r a b r b a

IsTotal 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 IsPreorder (α : Type u) (r : ααProp) extends , :

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

Instances
class IsTotalPreorder (α : Type u) (r : ααProp) extends , :

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

Instances
instance isTotalPreorder_isPreorder (α : Type u) (r : ααProp) [s : ] :

Every total pre-order is a pre-order.

Equations
class IsPartialOrder (α : Type u) (r : ααProp) extends , :

IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and IsAntisymm X r.

Instances
class IsLinearOrder (α : Type u) (r : ααProp) extends , :

IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and IsTotal X r.

Instances
class IsEquiv (α : Type u) (r : ααProp) extends , :

IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and IsSymm X r.

Instances
class IsStrictOrder (α : Type u) (r : ααProp) extends , :

IsStrictOrder X r means that the binary relation r on X is a strict order, that is, IsIrrefl X r and IsTrans X r.

Instances
class IsIncompTrans (α : Type u) (lt : ααProp) :
• incomp_trans : ∀ (a b c : α), ¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a

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

Instances
class IsStrictWeakOrder (α : Type u) (lt : ααProp) extends , :

IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and IsIncompTrans X lt.

Instances
class IsTrichotomous (α : Type u) (lt : ααProp) :
• trichotomous : ∀ (a b : α), lt a b a = b lt b a

IsTrichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

Instances
class IsStrictTotalOrder (α : Type u) (lt : ααProp) extends , :

IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, IsTrichotomous X lt and IsStrictOrder X lt.

Instances
instance eq_isEquiv (α : Type u) :
IsEquiv α fun x x_1 => x = x_1

Equality is an equivalence relation.

Equations
theorem irrefl {α : Type u} {r : ααProp} [inst : IsIrrefl α r] (a : α) :
¬r a a
theorem refl {α : Type u} {r : ααProp} [inst : IsRefl α r] (a : α) :
r a a
theorem trans {α : Type u} {r : ααProp} [inst : IsTrans α r] {a : α} {b : α} {c : α} :
r a br b cr a c
theorem symm {α : Type u} {r : ααProp} [inst : IsSymm α r] {a : α} {b : α} :
r a br b a
theorem antisymm {α : Type u} {r : ααProp} [inst : ] {a : α} {b : α} :
r a br b aa = b
theorem asymm {α : Type u} {r : ααProp} [inst : IsAsymm α r] {a : α} {b : α} :
r a b¬r b a
theorem trichotomous {α : Type u} {r : ααProp} [inst : ] (a : α) (b : α) :
r a b a = b r b a
theorem incomp_trans {α : Type u} {r : ααProp} [inst : ] {a : α} {b : α} {c : α} :
¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
instance isAsymm_of_isTrans_of_isIrrefl {α : Type u} {r : ααProp} [inst : IsTrans α r] [inst : IsIrrefl α r] :
IsAsymm α r
Equations
@[elab_without_expected_type]
theorem irrefl_of {α : Type u} (r : ααProp) [inst : IsIrrefl α r] (a : α) :
¬r a a
@[elab_without_expected_type]
theorem refl_of {α : Type u} (r : ααProp) [inst : IsRefl α r] (a : α) :
r a a
@[elab_without_expected_type]
theorem trans_of {α : Type u} (r : ααProp) [inst : IsTrans α r] {a : α} {b : α} {c : α} :
r a br b cr a c
@[elab_without_expected_type]
theorem symm_of {α : Type u} (r : ααProp) [inst : IsSymm α r] {a : α} {b : α} :
r a br b a
@[elab_without_expected_type]
theorem asymm_of {α : Type u} (r : ααProp) [inst : IsAsymm α r] {a : α} {b : α} :
r a b¬r b a
@[elab_without_expected_type]
theorem total_of {α : Type u} (r : ααProp) [inst : IsTotal α r] (a : α) (b : α) :
r a b r b a
@[elab_without_expected_type]
theorem trichotomous_of {α : Type u} (r : ααProp) [inst : ] (a : α) (b : α) :
r a b a = b r b a
@[elab_without_expected_type]
theorem incomp_trans_of {α : Type u} (r : ααProp) [inst : ] {a : α} {b : α} {c : α} :
¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
theorem isStrictWeakOrder_of_isTotalPreorder {α : Type u} {le : ααProp} {lt : ααProp} [inst : ] [inst : ] (h : ∀ (a b : α), lt a b ¬le b a) :
theorem lt_of_lt_of_incomp {α : Type u} {lt : ααProp} [inst : ] [inst : ] {a : α} {b : α} {c : α} :
lt a b¬lt b c ¬lt c blt a c
theorem lt_of_incomp_of_lt {α : Type u} {lt : ααProp} [inst : ] [inst : ] {a : α} {b : α} {c : α} :
¬lt a b ¬lt b alt b clt a c
theorem eq_of_incomp {α : Type u} {lt : ααProp} [inst : ] {a : α} {b : α} :
¬lt a b ¬lt b aa = b
theorem eq_of_eqv_lt {α : Type u} {lt : ααProp} [inst : ] {a : α} {b : α} :
¬lt a b ¬lt b aa = b
theorem incomp_iff_eq {α : Type u} {lt : ααProp} [inst : ] [inst : IsIrrefl α lt] (a : α) (b : α) :
¬lt a b ¬lt b a a = b
theorem eqv_lt_iff_eq {α : Type u} {lt : ααProp} [inst : ] [inst : IsIrrefl α lt] (a : α) (b : α) :
¬lt a b ¬lt b a a = b
theorem not_lt_of_lt {α : Type u} {lt : ααProp} [inst : ] {a : α} {b : α} :
lt a b¬lt b a