Documentation

Mathlib.Algebra.Order.GroupWithZero.Range

The range of a MonoidWithZeroHom #

Given a MonoidWithZeroHom f : A → B whose codomain B is a LinearOrderedCommGroupWithZero, we provide some order properties of the MonoidWithZeroHom.ValueGroup₀ as defined in Mathlib.Algebra.GroupWithZero.Range.

source
🔸 coverage
def MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHom {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] (f : A →*₀ B) :
ValueGroup₀ f →*₀o WithZero Bˣ

The inclusion of ValueGroup₀ f into WithZero Bˣ as a homomorphism of monoids with zero.

Instances For
    source
    📐 coverage
    theorem MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} :
    StrictMono ⇑(orderMonoidWithZeroHom f)
    source
    📐 coverage
    theorem MonoidWithZeroHom.ValueGroup₀.embedding_strictMono {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} :
    StrictMono ⇑embedding
    source
    📐 coverage
    instance MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} :
    IsOrderedMonoid (ValueGroup₀ f)
    source
    🔸 coverage
    @[implicit_reducible]
    instance MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} :
    LinearOrderedCommGroupWithZero (ValueGroup₀ f)
    source
    📐 coverage
    theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} (a : (ValueGroup₀ f)ˣ) :
    0 < embedding ↑a
    source
    theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [LinearOrderedCommGroupWithZero B] {f : A →*₀ B} (a : (ValueGroup₀ f)ˣ) :
    embedding ↑a ≠ 0