ofReal_div — Mathlib

English

For any real r,s and RCLike K, the real division embedded into K equals the direct division in K: ((r/s : ℝ) : K) = r/s and the reverse equality holds for division in the embedding sense.

Русский

Для любых действительных r,s и K, встроенное в K деление r/s равно самому делению в K: ((r/s : ℝ) : K) = r/s.

LaTeX

$$$$ ((r / s : \mathbb{R}) : K) = r / s. $$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_div (r s : ℝ) : ((r / s : ℝ) : K) = r / s :=
  map_div₀ (algebraMap ℝ K) r s

Похожие утверждения