instance NNRat.instAlgebra {α : Type u_2} [DivisionSemiring α] [CharZero α] : Algebra ℚ≥0 α

Equations

• NNRat.instAlgebra = Algebra.mk (NNRat.castHom α) ⋯ ⋯

instance NNRat.instlinearMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [DivisionSemiring α] [CharZero α] [DivisionSemiring β] [CharZero β] [FunLike F α β] [RingHomClass F α β] : LinearMapClass F ℚ≥0 α β

Equations

• ⋯ = ⋯

instance NNRat.instSMulCommClass {α : Type u_2} {β : Type u_3} [Semifield β] [CharZero β] [SMul α β] [SMulCommClass α β β] : SMulCommClass ℚ≥0 α β

Equations

• ⋯ = ⋯

instance NNRat.instSMulCommClass' {α : Type u_2} {β : Type u_3} [Semifield β] [CharZero β] [SMul α β] [SMulCommClass β α β] : SMulCommClass α ℚ≥0 β

Equations

• ⋯ = ⋯

theorem nnratCast_smul_eq_nnqsmul (α : Type u_2) {β : Type u_3} [Semifield α] [CharZero α] [Semiring β] [Module ℚ≥0 β] [Module α β] (q : ℚ≥0) (a : β) : ↑q • a = q • a

nnqsmul is equal to any other module structure via a cast.