Actions by nonnegative rational numbers

Scalar multiplication

@[instance_reducible, instance 100]

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

Equations

• NNRat.instDistribSMul = { toSMul := NNRat.smulDivisionSemiring, smul_zero := ⋯, smul_add := ⋯ }

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

@[instance_reducible, instance 100]

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

Equations

• Rat.instDistribSMul = { toSMul := Rat.smulDivisionRing, smul_zero := ⋯, smul_add := ⋯ }

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