Documentation

Mathlib.Algebra.Order.Monoid.Units

Units in ordered monoids #

instance AddUnits.instPreorderAddUnits {α : Type u_1} [inst : AddMonoid α] [inst : Preorder α] :
Equations
instance Units.instPreorderUnits {α : Type u_1} [inst : Monoid α] [inst : Preorder α] :
Equations
@[simp]
theorem AddUnits.val_le_val {α : Type u_1} [inst : AddMonoid α] [inst : Preorder α] {a : AddUnits α} {b : AddUnits α} :
a b a b
@[simp]
theorem Units.val_le_val {α : Type u_1} [inst : Monoid α] [inst : Preorder α] {a : αˣ} {b : αˣ} :
a b a b
@[simp]
theorem AddUnits.val_lt_val {α : Type u_1} [inst : AddMonoid α] [inst : Preorder α] {a : AddUnits α} {b : AddUnits α} :
a < b a < b
@[simp]
theorem Units.val_lt_val {α : Type u_1} [inst : Monoid α] [inst : Preorder α] {a : αˣ} {b : αˣ} :
a < b a < b
instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [inst : AddMonoid α] [inst : PartialOrder α] :
Equations
instance Units.instPartialOrderUnits {α : Type u_1} [inst : Monoid α] [inst : PartialOrder α] :
Equations
instance AddUnits.instLinearOrderAddUnits {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :
Equations
instance Units.instLinearOrderUnits {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :
Equations
def AddUnits.orderEmbeddingVal.proof_1 {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :
∀ {a b : AddUnits α}, { toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => u) } a { toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => u) } b { toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => u) } a { toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => u) } b
Equations
  • One or more equations did not get rendered due to their size.
def AddUnits.orderEmbeddingVal {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :

val : add_units α → α as an order embedding.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :
AddUnits.orderEmbeddingVal.toEmbedding = AddUnits.val
@[simp]
theorem Units.orderEmbeddingVal_apply {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :
Units.orderEmbeddingVal.toEmbedding = Units.val
def Units.orderEmbeddingVal {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :
αˣ ↪o α

val : αˣ → α as an order embedding.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddUnits.max_val {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] {a : AddUnits α} {b : AddUnits α} :
↑(max a b) = max a b
@[simp]
theorem Units.max_val {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] {a : αˣ} {b : αˣ} :
↑(max a b) = max a b
@[simp]
theorem AddUnits.min_val {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] {a : AddUnits α} {b : AddUnits α} :
↑(min a b) = min a b
@[simp]
theorem Units.min_val {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] {a : αˣ} {b : αˣ} :
↑(min a b) = min a b