Theorems · Theorem · field theory

DivisionSemiring.nnqsmul_def

∀ {K : Type u_2} [self : DivisionSemiring K] (q : ℚ≥0) (a : K), DivisionSemiring.nnqsmul q a = ↑q * a

However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast. Do not use this lemma directly. Use NNRat.smul_def instead.

Defined in

Mathlib.Algebra.Field.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionSemiring