Rescaling by a square root

For 0 ≤ a, multiplying by (√a)⁻¹ and squaring divides the square by a: ((√a)⁻¹ * x) ^ 2 = x ^ 2 / a. This is the change of variables x ↦ (√a)⁻¹ * x that turns the kernel 1 + x ^ 2 / a into 1 + y ^ 2.

Main results

• Real.inv_sqrt_mul_sq: ((√a)⁻¹ * x) ^ 2 = x ^ 2 / a for 0 ≤ a.

@[simp]

theorem Real.inv_sqrt_mul_sq {a : ℝ} (ha : 0 ≤ a) (x : ℝ) : ((√a)⁻¹ * x) ^ 2 = x ^ 2 / a

Multiplying by (√a)⁻¹ and squaring divides the square by a.