Theorems · Definition · field theory

DivisionRing.nnqsmul

{K : Type u_2} → [self : DivisionRing K] → ℚ≥0 → K → K

Scalar multiplication by a nonnegative rational number. Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def. Do not use directly. Instead use the • notation.

Defined in

Mathlib.Algebra.Field.Defs

Cited by

1 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Quot.sound

Assumes

DivisionRing