How to add NeZero to arbitrary field?

Stream: new members

[Arien Malec]

Or otherwise what incantations are required to make this work?

import Mathlib.Algebra.Field.Basic

variable {F: Type _}
variable [Field F]

example: (3: F) ≠ 0 := sorry

[Eric Wieser]

You can add [NeZero (3 : F)]

[Eric Wieser]

Or [CharZero F] if you want all numerals to be non-zero

[Arien Malec]

[CharZero F] is perfect. [NeZero (3: F)] feels like cheating :-)

[Eric Rodriguez]

Arien Malec said:

[CharZero F] is perfect. [NeZero (3: F)] feels like cheating :-)

I mean the first one implies the second :)

[Arien Malec]

This is for an Axler proof

example {v w: V}: ∃x, v + (3: F )•x = w := by
  use ((3⁻¹: F) • (w - v))
  rw [smul_smul, mul_inv_cancel, one_smul, add_comm, sub_add_cancel]
  exact three_ne_zero

where what we want is really the assertion that numerals act like numerals.... For extra credit, is there an induction or otherwise on an arbitrary field where I can show that example {v w: V} {a: F}: ∃x, v + a•x = w breaks down to cases where a = 0 and a \ne 0?

[Arien Malec]

(it's weird how quickly I forget in Lean that excluded middle is a thing).

[Arien Malec]

I guess that's also the same incantation and #mathlib documentation > NeZero.eq_zero_or_NeZero

[Kevin Buzzard]

by_cases ha : a = 0 will split you into two cases deoending on whether a is 0 or not (and probably something like obtain \<rfl, ha\> := eq_or_ne a 0 will do it more efficiently if I got it right)

[Arien Malec]

In other news, the whole proof doesn't work if a = 0 :--)

[Ruben Van de Velde]

obtain rfl|ha := ...