Inhabited Field

Stream: Is there code for X?

[Bolton Bailey]

import Mathlib.FieldTheory.SplittingField.Construction

lemma foo (F) [Field F] (l : List F) : F := l.get! 0
-- failed to synthesize instance Inhabited F

Where can I find an instance of inhabited for Field?

[Adam Topaz]

import Mathlib

variable (F : Type*) [Field F]

#synth (Inhabited F)

comes up short for me!

[Adam Topaz]

I suppose you could use docs#List.getD instead

[Eric Wieser]

I think it would probably be safe to add this, but it wouldn't be safe for Monoid or AddMonoid

[Eric Wieser]

(as if we had both there would be a diamond for Ring)