toLinearOrderedCommGroupWithZero — Mathlib

English

If α is a canonically ordered semifield, there exists a LinearOrderedCommGroupWithZero structure on α that is compatible with its existing order and algebraic operations.

Русский

Если α — канонически упорядоченная полупольность, существует структура LinearOrderedCommGroupWithZero на α, совместимая с имеющимся порядком и алгебраическими операциями.

LaTeX

$$$\\exists G \;\\text{LinearOrderedCommGroupWithZero }\\alpha$$$

Lean4

/-- Construct a `LinearOrderedCommGroupWithZero` from a canonically linear ordered semifield. -/
abbrev toLinearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero α
    where
  __ := ‹Semifield α›
  __ := ‹LinearOrder α›
  bot := 0
  bot_le := zero_le
  zero_le_one := zero_le_one
  mul_le_mul_left := fun _ _ h _ ↦ mul_le_mul_of_nonneg_left h <| zero_le _

Похожие утверждения