How does one actually create a field?

Stream: mathlib4

[Cody Roux]

Newbie question: how does one "actually" declare a field? It has a lot of structure, with a bunch of mixins, and I see that R's structure is created with infer_instance (not sure what's that doing). What is the right way to do this?

[Cody Roux]

side note: what does infer_instance do?

[Floris van Doorn]

infer_instance is just running type-class inference. Is is concluded from LinearOrderedField ℝ a few lines higher.

[Floris van Doorn]

It depends on what you're doing how you most conveniently define a new field. In Mathlib we generally give AddGroup/Ring/... instances first (often under weaker conditions), before giving the field instance.

[Floris van Doorn]

If you want to give all the fields, you can write _ and click on the lightbulb
image.png
(PS: This is the first time I see the minimal skeleton option, that is an amazing new option!)

[Floris van Doorn]

If you have an injective map into an existing field, docs#Function.Injective.field can be useful.

[Cody Roux]

Thanks @Floris van Doorn ! I'm trying to build a non-standard version of R, using model theory. Indeed I think you originally worked on that lib?

Sadly I think there's no injection into R or anything.