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.

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

coe : αˣ → α as an order embedding.

Equations
source
@[simp]
theorem units.order_embedding_coe_apply {α : Type u_1} [monoid α] [linear_order α] :
⇑units.order_embedding_coe = coe
source
@[simp]
theorem add_units.order_embedding_coe_apply {α : Type u_1} [add_monoid α] [linear_order α] :
⇑add_units.order_embedding_coe = coe
source
def add_units.order_embedding_coe {α : Type u_1} [add_monoid α] [linear_order α] :
add_units α ↪o α

coe : add_units α → α as an order embedding.

Equations
source
@[simp, norm_cast]
theorem add_units.max_coe {α : Type u_1} [add_monoid α] [linear_order α] {a b : add_units α} :
↑(linear_order.max a b) = linear_order.max ↑a ↑b
source
@[simp, norm_cast]
theorem units.max_coe {α : Type u_1} [monoid α] [linear_order α] {a b : αˣ} :
↑(linear_order.max a b) = linear_order.max ↑a ↑b
source
@[simp, norm_cast]
theorem units.min_coe {α : Type u_1} [monoid α] [linear_order α] {a b : αˣ} :
↑(linear_order.min a b) = linear_order.min ↑a ↑b
source
@[simp, norm_cast]
theorem add_units.min_coe {α : Type u_1} [add_monoid α] [linear_order α] {a b : add_units α} :
↑(linear_order.min a b) = linear_order.min ↑a ↑b