Reflection of z in a1 about a1

Stream: new members

[Shadman Sakib]

How do I show that reflection a1 of z = z, where z is in a1?

[Shadman Sakib]

import analysis.complex.circle
import analysis.normed_space.inner_product

noncomputable theory

open complex
variables {V : Type*} [inner_product_space ℂ V]

lemma same_point (a₁ : subspace ℝ V) [complete_space a₁] (z : V) (h: z ∈ a₁) : reflection (a₁) z = z :=
begin
  sorry,
end

[Kyle Miller]

I'm not sure if it's because I don't have the same version of mathlib, but I don't seem to have reflection. Where is it defined?

[Shadman Sakib]

Ah yeah, you know what, someone is adding reflection to the library. I have their version of math lib, sorry

[Shadman Sakib]

I will update this stream when reflection is added