Documentation

Mathlib.Algebra.Ring.Action.Rat

Actions by nonnegative rational numbers #

Scalar multiplication #

source
🔸 coverage
@[implicit_reducible, instance 100]
instance NNRat.instDistribSMul {R : Type u_1} [DivisionSemiring R] :
DistribSMul ℚ≥0 R
source
📐 coverage
instance NNRat.instIsScalarTowerRight {R : Type u_1} [DivisionSemiring R] :
IsScalarTower ℚ≥0 R R
source
🔸 coverage
@[implicit_reducible, instance 100]
instance Rat.instDistribSMul {R : Type u_1} [DivisionRing R] :
DistribSMul ℚ R
source
📐 coverage
instance Rat.instIsScalarTowerRight {R : Type u_1} [DivisionRing R] :
IsScalarTower ℚ R R