mathlib3 documentation

algebra.order.monoid.units

Units in ordered monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def add_units.preorder {α : Type u_1} [add_monoid α] [preorder α] :
Equations
@[protected, instance]
def units.preorder {α : Type u_1} [monoid α] [preorder α] :
Equations
@[simp, norm_cast]
theorem add_units.coe_le_coe {α : Type u_1} [add_monoid α] [preorder α] {a b : add_units α} :
a b a b
@[simp, norm_cast]
theorem units.coe_le_coe {α : Type u_1} [monoid α] [preorder α] {a b : αˣ} :
a b a b
@[simp, norm_cast]
theorem add_units.coe_lt_coe {α : Type u_1} [add_monoid α] [preorder α] {a b : add_units α} :
a < b a < b
@[simp, norm_cast]
theorem units.coe_lt_coe {α : Type u_1} [monoid α] [preorder α] {a b : αˣ} :
a < b a < b
@[protected, instance]
Equations
@[protected, instance]
def units.linear_order {α : Type u_1} [monoid α] [linear_order α] :
Equations
def units.order_embedding_coe {α : Type u_1} [monoid α] [linear_order α] :
αˣ ↪o α

coe : αˣ → α as an order embedding.

Equations

coe : add_units α → α as an order embedding.

Equations
@[simp, norm_cast]
@[simp, norm_cast]
theorem units.max_coe {α : Type u_1} [monoid α] [linear_order α] {a b : αˣ} :
@[simp, norm_cast]
theorem units.min_coe {α : Type u_1} [monoid α] [linear_order α] {a b : αˣ} :
@[simp, norm_cast]