Stream: new members

Topic: How to add NeZero to arbitrary field?

Arien Malec (Dec 08 2023 at 16:54):

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 (Dec 08 2023 at 16:56):

You can add [NeZero (3 : F)]

Eric Wieser (Dec 08 2023 at 16:57):

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

Arien Malec (Dec 08 2023 at 17:02):

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

Eric Rodriguez (Dec 08 2023 at 17:04):

Arien Malec said:

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

I mean the first one implies the second :)

Arien Malec (Dec 08 2023 at 17:09):

This is for an Axler proof

example {v w: V}: ∃x, v + (3: F )•x = w := by
use ((3⁻¹: F) • (w - v))
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 (Dec 08 2023 at 17:14):

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

Arien Malec (Dec 08 2023 at 17:17):

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

Kevin Buzzard (Dec 08 2023 at 18:23):

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 (Dec 08 2023 at 18:38):

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

Ruben Van de Velde (Dec 08 2023 at 18:55):

obtain rfl|ha := ...

Last updated: Dec 20 2023 at 11:08 UTC