Zulip Chat Archive

Stream: condensed mathematics

Topic: 1/2 is not canonical

Kevin Buzzard (Apr 30 2022 at 02:58):

Recently to abuse defeq I changed a definition in LTE and had to do quite a big refactor. I learnt how to get automation to help me, but one thing I noticed was that simp simps 1 / 2 to 2⁻¹ in both real and nnreal, which made it harder to use the simplifier -- stuff wasn't in simp normal form. On a whim, I just spent the last few hours changing all the 1/2s in the project to 2⁻¹s. I think it's better. I think half could refer to this constant, Most proof fixes just involved removing \l one_div stuff. My logic: if we were using -1 constantly in an argument we wouldn't keep writing 0 - 1 would we!

The refactor is on the twoinv branch, which I didn't merge to master. Note @Johan Commelin I changed the "front facing" challenge.lean. Are there aesthetic reasons why you'd prefer mathematicians to see the horrible 1 / 2? Does anyone have any comments about this? Should I make a PR?

Kevin Buzzard (Apr 30 2022 at 03:27):

The diff is here. Everything gets a bit shorter.

Kevin Buzzard (Apr 30 2022 at 03:41):

I suspect that some proofs could be golfed now.

Johan Commelin (Apr 30 2022 at 04:12):

@Kevin Buzzard Thanks! I'm perfectly fine with having 2⁻¹ everywhere.

Yaël Dillies (Apr 30 2022 at 06:15):

I just replaced (2⁻¹) by 2⁻¹ everywhere, because ⁻¹ has maximal precedence.

Johan Commelin (Apr 30 2022 at 06:18):

In the branch, I guess?

Johan Commelin (Apr 30 2022 at 06:19):

Ok, I have now pushed a commit that merges twoinv into master.

Johan Commelin (Apr 30 2022 at 06:19):

Thanks to both of you for this polishing.

Kevin Buzzard (Apr 30 2022 at 09:37):

Thanks Yael!

Eric Wieser (Apr 30 2022 at 11:00):

I guess docs#exp_series should be redefined to use inv instead of div too?

Kevin Buzzard (Apr 30 2022 at 12:35):

My memory was that Ashvni and I had an awful time manipulating the algebra when doing Bernouilli polynomials via power series. Maybe this would have made it easier?

Filippo A. E. Nuccio (Apr 30 2022 at 13:05):

I take my share of responsibility for inserting (1 / 2)all over the places and not reverting it back as soon as I realised that many lemmas where rather stated with 2⁻¹ and that simpwas keeping on inserting some div_one_eq_inv at all places. I am sorry. :division:

Kevin Buzzard (Apr 30 2022 at 13:07):

Fortunately global search and replace is not hard to use :-)

Yaël Dillies (Apr 30 2022 at 13:11):

Welp, looks like this issue doesn't divide us!

Last updated: Dec 20 2023 at 11:08 UTC