English
Casting a scientific literal via ℚ is the same as casting directly into a Division Ring K.
Русский
Приведение научной записи через ℚ такое же, как приведение напрямую в кольцо деления K.
LaTeX
$$$ \forall K [\mathrm{DivisionRing}\,K], \left( \mathrm{OfScientific.ofScientific}(m,s,e) : \mathbb{Q} \right) = \left( \mathrm{OfScientific.ofScientific}(m,s,e) : K \right). $$$
Lean4
/-- Casting a scientific literal via `ℚ` is the same as casting directly. -/
@[simp, norm_cast]
theorem cast_ofScientific {K} [DivisionRing K] (m : ℕ) (s : Bool) (e : ℕ) :
(OfScientific.ofScientific m s e : ℚ) = (OfScientific.ofScientific m s e : K) := by
rw [← NNRat.cast_ofScientific (K := K), ← NNRat.cast_ofScientific, cast_nnratCast]
