# Zulip Chat Archive

## Stream: maths

### Topic: Instances for is_R_or_C

#### Heather Macbeth (Dec 20 2020 at 22:38):

I learned the other day that typeclass inference finds the `complete_space`

and `proper_space`

instances for finite-dimensional normed spaces over both `ℝ`

and `ℂ`

by typeclass inference.

Sebastien Gouezel said:

Over the reals, it's already registered as an instance.

`example {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] : complete_space E := by apply_instance`

(through docs#finite_dimensional.proper_real). It also applies over the complexes as all the instances to see a complex vector space as a real vector space are already there:

`example {E : Type*} [normed_group E] [normed_space ℂ E] [finite_dimensional ℂ E] : complete_space E := by apply_instance`

question 1: It should be safe to register

```
variables {𝕜 : Type*} [is_R_or_C 𝕜]
instance {E : Type*} [normed_group E] [normed_space 𝕜 E] [finite_dimensional 𝕜 E] : complete_space E := ...
```

right? Since `complete_space`

is Prop-valued, so there is no concern about duplicate instances. Same for `proper_space`

.

question 2: Assuming it's safe, how do I do fill in the proof, since the proofs for `ℝ`

and `ℂ`

are a little different? Does `is_R_or_C`

allow me to split into cases? @Frédéric Dupuis

#### Frédéric Dupuis (Dec 20 2020 at 23:38):

Yes, we definitely want the instance for `is_R_or_C`

, otherwise we can't use it to prove results for both `ℝ`

and `ℂ`

that require `complete_space`

. The challenge is going to be to make sure that this instance is defeq with the existing ones in both cases.

#### Heather Macbeth (Dec 20 2020 at 23:38):

But in this case it shouldn't matter about being defeq, right? Because `complete_space`

is Prop-valued, no data.

#### Frédéric Dupuis (Dec 20 2020 at 23:39):

Ah, right!

#### Frédéric Dupuis (Dec 20 2020 at 23:39):

Do you know where those two instances are defined?

#### Heather Macbeth (Dec 20 2020 at 23:39):

So how do I prove this? :). Can I break into cases somehow?

#### Heather Macbeth (Dec 20 2020 at 23:40):

Frédéric Dupuis said:

Do you know where those two instances are defined?

Taking `proper`

first (since `complete`

is deduced from that), it's just docs#finite_dimensional.proper_real.

#### Frédéric Dupuis (Dec 20 2020 at 23:40):

There's one of the axioms of `is_R_or_C`

that can effectively be used to break into cases, but it won't be type equality.

#### Heather Macbeth (Dec 20 2020 at 23:41):

Using, for C, that a finite-dimensional space over C is also finite-dimensional over R.

#### Frédéric Dupuis (Dec 20 2020 at 23:42):

Ah, then we should be able to do this as well without needing to break in into cases.

#### Heather Macbeth (Dec 20 2020 at 23:43):

(the latter is docs#finite_dimensional.complex_to_real apparently)

#### Frédéric Dupuis (Dec 20 2020 at 23:44):

For instance this sort of trick is used here: https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/inner_product.html#exists_norm_eq_infi_of_complete_subspace

#### Heather Macbeth (Dec 20 2020 at 23:44):

Great, thank you!

#### Heather Macbeth (Dec 21 2020 at 00:06):

OK, I can do this:

```
import analysis.normed_space.finite_dimension
import data.complex.is_R_or_C
variables {𝕜 : Type*} [is_R_or_C 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
instance finite_dimensional.is_R_or_C_to_real : finite_dimensional ℝ 𝕜 := sorry
instance finite_dimensional.proper_is_R_or_C [finite_dimensional 𝕜 E] : proper_space E :=
begin
letI : normed_space ℝ E := restrict_scalars.normed_space ℝ 𝕜 E,
letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
letI : finite_dimensional ℝ E := finite_dimensional.trans ℝ 𝕜 E,
apply_instance
end
```

but how do I fill in the sorry? We don't seem to have that `is_R_or_C`

is finite-dimensional over `ℝ`

, and presumably this instance, though safe to add to the library, will have a proof involving breaking into cases.

#### Frédéric Dupuis (Dec 21 2020 at 00:16):

Hmm... good question!

#### Heather Macbeth (Dec 21 2020 at 00:40):

I could probably prove it directly from docs#is_R_or_C.re_add_im_ax, would that be a hack?

#### Frédéric Dupuis (Dec 21 2020 at 00:52):

I wouldn't say it's a hack, I think that's how it should be done!

#### Frédéric Dupuis (Dec 21 2020 at 00:53):

I think this together with `finite_dimensional.iff_fg`

(and probably a lot of fiddling around...) will do the trick.

#### Heather Macbeth (Dec 21 2020 at 05:35):

Last updated: May 09 2021 at 10:11 UTC