linarith with complex numbers?

Stream: new members

[Sabbir Rahman]

linarith works pretty well with reals, but doesn't work with complex numbers. What is the reason for this and then what to do for simple cases like below?

import Mathlib

example (x : ℝ) (h: x - 1 = 0) : x = 1 := by linarith
example (x : ℂ) (h: x - 1 = 0) : x = 1 := by linarith  -- didn't succeed

[Yakov Pechersky]

The complexes don't have a linear order instance, and linarith is for _lin_ear orders. The complexes can have a linear order, but not one that is compatible with the field structure.

[Vlad Tsyrklevich]

  have := Complex.ext_iff.mp h
  simp at this
  apply Complex.ext <;> simp <;> linarith

or

  apply (@sub_left_inj _ _ 1).mp
  simp [h]

[Riccardo Brasca]

It may be an overkill, but I guess polyrith works.

[Sabbir Rahman]

Yakov Pechersky said:

The complexes don't have a linear order instance, and linarith is for _lin_ear orders. The complexes can have a linear order, but not one that is compatible with the field structure.

ah makes sense

[Sabbir Rahman]

I generally prefer overkill methods over trying to remember theorem names. NO matter how much I try, I can't remember the theorem for my particular case

[Vlad Tsyrklevich]

You don't have to remember all of the names. I don't.

extensionality theorems tell you that if the components of something are equal, then the whole object is equal. That's the first approach, I just reduce proving equality over C to proving 2 equalities in R. Findable by loogling: Complex, "ext"

Otherwise, how would you prove that x - 1 = 0 implies x = 1? In school you would just write +1 on both sides of the equation and simplify. But _why_ can you do that? Because addition/subtraction is injective, so you can add/subtract quantities to both sides of an equation and it remains true. Hence you can search for an injectivity theorem for subtraction. Findable by loogling: "sub_", "inj"