half_eq_one_div_two

Stream: Is there code for X?

[Iván Renison]

Hi, do you know how can I probe this?

example : (0.5 : ℝ) = 1/2 := sorry

[Adam Topaz]

by norm_num.

[Iván Renison]

With norm_num I get the in goal 0.5 = 2⁻¹

[Adam Topaz]

It works for me:

import Mathlib

example : (0.5 : ℝ) = 1/2 := by norm_num

[Adam Topaz]

by hint says that by bound works as well. you could try that instead.

[Iván Renison]

Ah, okay, I was not importing the hole of Mathlib, that's why it didn't work for me

[Iván Renison]

Do you know what should I import if I want to use it with out having to import the whole Mathlib?

[Damiano Testa]

#min_imports will tell you:

import Mathlib

lemma X : (0.5 : ℝ) = 1/2 := by norm_num

#min_imports -- import Mathlib.Analysis.RCLike.Basic

[Iván Renison]

Great! I didn't know about #min_imports. Thank you very much!

[Violeta Hernández]

I think the real answer is, why are you writing 0.5 to begin with?

[Iván Renison]

I'm trying to formalize a math olympiad problem

[Iván Renison]

You think I should directly use 1/2?

[Violeta Hernández]

I think you should directly use 2⁻¹ but 1/2 is probably fine too.

[Iván Renison]

Ok, thank you