Actions by nonnegative rational numbers

Scalar multiplication

@[instance 100]

instance NNRat.instDistribSMul {R : Type u_1} [DivisionSemiring R] : DistribSMul ℚ≥0 R

Equations

• NNRat.instDistribSMul = DistribSMul.mk ⋯

instance NNRat.instIsScalarTowerRight {R : Type u_1} [DivisionSemiring R] : IsScalarTower ℚ≥0 R R

@[instance 100]

instance Rat.instDistribSMul {R : Type u_1} [DivisionRing R] : DistribSMul ℚ R

Equations

• Rat.instDistribSMul = DistribSMul.mk ⋯

instance Rat.instIsScalarTowerRight {R : Type u_1} [DivisionRing R] : IsScalarTower ℚ R R