Antilinear functions over the reals

Stream: maths

[Daniel Roca González]

Hello everyone,
I'm working over a real Hilbert space E and want to use the Riesz representation lemma. inner_product_space.to_dual from mathlib gives me an equivalence E ≃ₛₗᵢ[↑conj] normed_space.dual 𝕜 E, from which one can get an antilinear map normed_space.dual ℝ E →ₛₗ[↑conj] E. How can I get a linear map from this? I'm not sure how to begin...

[Heather Macbeth]

@Daniel Roca González It is designed to "just work". An antilinear map over ℝ is definitionally a linear map.

[Heather Macbeth]

import analysis.inner_product_space.dual

noncomputable theory

variables {E : Type*} [inner_product_space ℝ E] [complete_space E]

example : E ≃ₗᵢ[ℝ] normed_space.dual ℝ E := inner_product_space.to_dual ℝ E

[Daniel Roca González]

wow I can't believe I didn't try this, thank you. Yeah this works just fine.

[Heather Macbeth]

If you'd like to know more:
https://leanprover-community.github.io/blog/posts/semilinear-maps/

[Daniel Roca González]

Thanks a lot. I think I had understood that linear maps are defined as semilinear maps, but I somehow didn't make the connection that ↑conj is equal to the identity definitionally