# Zulip Chat Archive

## Stream: new members

### Topic: question on is_R_or_C

#### Monica Omar (Feb 06 2023 at 09:32):

When dealing with `is_R_or_C 𝕜`

, is there a way to "separate" it in the proof? Like proving it in the case of `𝕜 = ℝ`

and in the case of `𝕜 = ℂ`

?

#### Yaël Dillies (Feb 06 2023 at 09:56):

Not really, no. That's the entire point of `is_R_or_C`

in the first place : avoid proving every real and complex result separately.

#### Ruben Van de Velde (Feb 06 2023 at 10:08):

You might be able to case on `I = 0`

; not sure if that would help

#### Eric Wieser (Feb 06 2023 at 12:48):

Yes, that's docs#is_R_or_C.I_mul_I_ax

#### Jireh Loreaux (Feb 06 2023 at 16:25):

I think a key question is: why do you *want* to separate it? I'm not saying there are no possible reasons, but often it's the case that there is a better way to work with `is_R_or_C`

.

#### Monica Omar (Feb 07 2023 at 12:14):

For example, if I want to show that any self-adjoint linear map `T`

has the property: `(∀ x, ⟪x, T x⟫ = 0) ↔ T = 0`

, then I wanted to see if I can use `inner_map_self_eq_zero`

for the complex case, instead of copying the proof.

#### Eric Wieser (Feb 07 2023 at 12:48):

Arguably docs#inner_map_self_eq_zero should be stated for `is_R_or_C`

in the first place

#### Monica Omar (Feb 07 2023 at 13:56):

you need the self-adjoint property for it to work over the reals though

#### Eric Wieser (Feb 07 2023 at 14:17):

Can you give the full statement of what you want to prove?

#### Kyle Miller (Feb 07 2023 at 14:32):

Eric Wieser said:

Arguably docs#inner_map_self_eq_zero should be stated for

`is_R_or_C`

in the first place

Isn't that false over R? For example, have V be R^2 and T be rotation by a quarter turn.

#### Monica Omar (Feb 07 2023 at 14:49):

Eric Wieser said:

Can you give the full statement of what you want to prove?

Here ya go

```
import analysis.inner_product_space.symmetric
variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
local notation `⟪`x`,`y`⟫` := @inner 𝕜 _ _ x y
example (T : E →ₗ[𝕜] E) (hT : T.is_symmetric) :
(∀ x, ⟪x, T x⟫ = 0) ↔ T = 0 :=
sorry
```

#### Jireh Loreaux (Feb 07 2023 at 16:04):

You could prove something like this that works over `is_R_or_C`

.

```
import analysis.inner_product_space.symmetric
variables {𝕜 V : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 V]
open is_R_or_C
local notation `⟪` x `, ` y `⟫` := @inner 𝕜 _ _ x y
lemma linear_map.is_symmetric.inner_map_polarization {T : V →ₗ[𝕜] V} (hT : T.is_symmetric)
(x y : V) :
⟪ T x, y ⟫ = (⟪T (x + y) , x + y⟫ - ⟪T (x - y) , x - y⟫ -
I * ⟪T (x + (I : 𝕜) • y) , x + (I : 𝕜) • y⟫ +
I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y ⟫) / 4 :=
begin
rcases @I_mul_I_ax 𝕜 _ with (h | h),
{ simp only [h, map_add, map_sub, add_zero, zero_mul, sub_zero],
simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right],
rw [hT y x, ←inner_conj_sym y (T x), eq_conj_iff_re.mpr _],
{ ring, },
{ nth_rewrite 1 ←re_add_im (⟪T x, y⟫),
rw [h, mul_zero, add_zero] } },
{ simp only [map_add, map_sub, inner_add_left, inner_add_right, linear_map.map_smul,
inner_smul_left, inner_smul_right, is_R_or_C.conj_I, ←pow_two, sq, h,
inner_sub_left, inner_sub_right, mul_add, ←mul_assoc, mul_neg, neg_neg,
sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub],
ring, }
end
example {T : V →ₗ[𝕜] V} (hT : T.is_symmetric) :
(∀ x, ⟪T x, x⟫ = 0) ↔ T = 0 :=
begin
refine ⟨λ h, _, λ h, by simp only [h, linear_map.zero_apply, inner_zero_left, forall_const]⟩,
ext x,
rw [linear_map.zero_apply, ←inner_self_eq_zero, hT.inner_map_polarization],
simp only [h _],
ring,
end
```

#### Monica Omar (Feb 07 2023 at 16:05):

Jireh Loreaux said:

You could prove something like this that works over

`is_R_or_C`

.`import analysis.inner_product_space.symmetric variables (𝕜 V : Type*) [is_R_or_C 𝕜] [inner_product_space 𝕜 V] open is_R_or_C local notation `⟪` x `, ` y `⟫` := @inner 𝕜 _ _ x y lemma is_symmetric.inner_map_polarization (T : V →ₗ[𝕜] V) (x y : V) (hT : T.is_symmetric): ⟪ T x, y ⟫ = (⟪T (x + y) , x + y⟫ - ⟪T (x - y) , x - y⟫ - I * ⟪T (x + (I : 𝕜) • y) , x + (I : 𝕜) • y⟫ + I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y ⟫) / 4 := begin rcases @I_mul_I_ax 𝕜 _ with (h | h), { simp only [h, map_add, map_sub, add_zero, zero_mul, sub_zero], simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right], rw [hT y x, ←inner_conj_sym y (T x), eq_conj_iff_re.mpr _], { ring, }, { nth_rewrite 1 ←re_add_im (⟪T x, y⟫), rw [h, mul_zero, add_zero] } }, { simp only [map_add, map_sub, inner_add_left, inner_add_right, linear_map.map_smul, inner_smul_left, inner_smul_right, is_R_or_C.conj_I, ←pow_two, sq, h, inner_sub_left, inner_sub_right, mul_add, ←mul_assoc, mul_neg, neg_neg, sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub], ring, } end`

yo! I was legit in the process of doing this - haha!

#### Jireh Loreaux (Feb 07 2023 at 16:26):

(edited the code above with a proof of your result)

#### Jireh Loreaux (Feb 07 2023 at 16:33):

Actually, if you want to PR the results above, that would be nice.

#### Monica Omar (Feb 07 2023 at 16:35):

yeah! sounds good. i'll do that just now. i'll have to give your code the credit tho lol

#### Jireh Loreaux (Feb 07 2023 at 16:48):

no need, don't worry about it.

Last updated: Dec 20 2023 at 11:08 UTC