Documentation
Mathlib
.
Algebra
.
Order
.
Module
.
Rat
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Order.Module.Defs
Mathlib.Data.Rat.Cast.Order
Imported by
abs_nnqsmul
abs_qsmul
LinearOrderedSemifield
.
toPosSMulStrictMono_rat
LinearOrderedField
.
toPosSMulStrictMono_rat
Monotonicity of the action by rational numbers
#
source
@[simp]
theorem
abs_nnqsmul
{α :
Type
u_1}
[
LinearOrderedAddCommGroup
α
]
[
DistribMulAction
ℚ≥0
α
]
[
PosSMulMono
ℚ≥0
α
]
(q :
ℚ≥0
)
(a :
α
)
:
|
q
•
a
|
=
q
•
|
a
|
source
@[simp]
theorem
abs_qsmul
{α :
Type
u_1}
[
LinearOrderedAddCommGroup
α
]
[
Module
ℚ
α
]
[
PosSMulMono
ℚ
α
]
(q :
ℚ
)
(a :
α
)
:
|
q
•
a
|
=
|
q
|
•
|
a
|
source
instance
LinearOrderedSemifield
.
toPosSMulStrictMono_rat
{α :
Type
u_1}
[
LinearOrderedSemifield
α
]
:
PosSMulStrictMono
ℚ≥0
α
Equations
⋯
=
⋯
source
instance
LinearOrderedField
.
toPosSMulStrictMono_rat
{α :
Type
u_1}
[
LinearOrderedField
α
]
:
PosSMulStrictMono
ℚ
α
Equations
⋯
=
⋯