sqrt_intCast — Mathlib

English

For any integer z, Rat.sqrt(z) equals Int.sqrt(z) (as a rational).

Русский

Для любого целого z квадратный корень Ratsqrt(z) равен Int.sqrt(z) (с математическим приводением).

LaTeX

$$$ \operatorname{Rat.sqrt}(z) = \operatorname{Int.sqrt}(z) $$$

Lean4

@[simp, norm_cast]
theorem sqrt_intCast (z : ℤ) : Rat.sqrt (z : ℚ) = Int.sqrt z := by
  simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]

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