extends keyword

Stream: new members

[Calle Sönne]

Hello,

I want to make an instance of a class which extends 3 other classes (and contains no other fields). Specifically this one:

class reflective (R : D ⥤ C) extends is_right_adjoint R, full R, faithful R.

I have proven that my functor is an instance of each of is_right_adjoint R, full R, faithful R..
Is there a way for me to prove this using the prior instances? Or should I just incorporate their proofs into this one?
When I use the "generate skeleton for fields" feature it also expands is_right_adjoint, full and faithful into their fields.

[Eric Wieser]

{ .. right_adjoint_proof, .. full_proof, ..faithful_proof }

[Eric Wieser]

Note that instance names are fully-qualified (protected), so the proof will typically be namespace.instance_name

[Kevin Buzzard]

It's nice to know such classes exist already in lean. Number fields are a class which extends three classes (field, Q-algebra, finite-dimensional) and I was concerned that people would argue that if I wanted a number field i should ask for those classes instead

[Eric Wieser]

An argument against this type of class is that you'll often assume it even though you actually just need one of its pieces -
a lot of lemmas about docs#integral_domain are actually just about docs#no_zero_divisors

[Kevin Buzzard]

An argument for them is that if you tell a number theorist that they have to write three lines of gobble-de-gook every time they want a number field, this is not going to go down well. You can just as well argue that we shouldn't have a ring class, we should just have mixin after mixin.

[Kevin Buzzard]

Structures central to mathematics should be there, whatever the computer scientists think of them.

[Julian Külshammer]

Hopefully by the time number field will be used in mathlib extensively, Alex' new linter will be ready and it will tell you if you assumed number field but only needed finite-dimensional.