Zulip Chat Archive

Stream: maths

Topic: field_simp fails

Yury G. Kudryashov (Dec 19 2019 at 22:14):

Hi, field_simp fails to simplify y = (y - x) / (z - x) * z + (1 - (y - x) / (z - x)) * x. It gives y = (y + -x) * z / (z + -x) + (1 + (x + -y) / (z + -x)) * x. It seems that it lacks a + b / c = (a * c + b) / c rule.

Yury G. Kudryashov (Dec 19 2019 at 22:18):

Sorry, adding h : z + -x ≠ 0 did the trick (didn't work with z - x ≠ 0).

Kevin Buzzard (Dec 19 2019 at 22:22):

aah, the dreaded sub_eq_add_neg strikes again!

Yury G. Kudryashov (Dec 19 2019 at 22:24):

Possibly field_simp should (partially) simplify its arguments first.

Yury G. Kudryashov (Dec 19 2019 at 22:24):

Without sub_eq_add_neg we would need separate lemmas for a - b / c etc.

Kevin Buzzard (Dec 19 2019 at 22:25):

Yes, it is somehow a necessary evil sometimes

Last updated: Dec 20 2023 at 11:08 UTC