Working with rationals

Stream: new members

[Nathan]

How do I work with rationals? I don't know how to do something as simple as:

example : (1+3:ℚ) = (4:ℚ) := by
  refine Rat.ext ?_ ?_
  · sorry
  · sorry

[Nathan]

simp doesn't work

[Ruben Van de Velde]

norm_num should work

[Nathan]

aha, thanks :pray:

[Nathan]

what about this? example (a b : ℚ) : a*b/a = b := sorry

[Ruben Van de Velde]

It's not true! (If a is zero)

[Ruben Van de Velde]

But I'd hope that by apply? finds something useful

[Nathan]

oh yeah true, if i add the hypothesis then maybe that will help apply? out

[Alfredo Moreira-Rosa]

yes, try this:

import Batteries.Data.Rat
import Mathlib.Data.Rat.Lemmas
import Mathlib.Tactic

example (a b : ℚ) (h:a ≠ 0) : a * b / a = b := by field_simp

[Alfredo Moreira-Rosa]

or using exact?, you get :

example (a b : ℚ) (h:a ≠ 0) : a * b / a = b := by exact mul_div_cancel_left₀ b h

[Nathan]

oh field_simp is great, thanks

[Alfredo Moreira-Rosa]

in the same vein of field_simp, you have ring, noncomm_ring, module, abel, group depending on your use case.

[Alfredo Moreira-Rosa]

to find which one solves your goal, you can use hint or try?. try? will come up with more complex tactics than hint in my experience

[Nathan]

i feel like i'm starting to get the hang of this

[Nathan]

maybe i'll just post here rather than open a new topic...

is there any way to convert a sum over a Fin into a sum over a Finset? I wrote half my code one way, and half the other. now i need to connect them...

example (k : ℕ) (f : ℕ → ℚ) : ∑ i ∈ Finset.Ico 0 k, f i = ∑ i : Fin k, f i := sorry

[Aaron Liu]

Nathan said:

maybe i'll just post here rather than open a new topic...

is there any way to convert a sum over a Fin into a sum over a Finset? I wrote half my code one way, and half the other. now i need to connect them...

example (k : ℕ) (f : ℕ → ℚ) : ∑ i ∈ Finset.Ico 0 k, f i = ∑ i : Fin k, f i := sorry

docs#Finset.sum_range and docs#Finset.range_eq_Ico

[Nathan]

oh wow, thanks :pray: thought i would have to rewrite it so everything was in Finsets :sweat_smile: probably should anyway, but i just want to get it working first

[Nathan]

why might i get Unknown identifier 'range'? i'm importing all of Mathlib

[Nathan]

oh duh i just need Finset.range