Theorems · Theorem · number theory

NNRatCast.ofScientific_eq_ite

∀ {K : Type u_1} [inst : NNRatCast K] (m : ℕ) (b : Bool) (d : ℕ),
  OfScientific.ofScientific m b d = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Defined in

Mathlib.Algebra.Field.Rat

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NNRatCast