Casts to fields

Stream: general

[Yaël Dillies]

It seems that some/many results in mathlib use ℚ in place of char zero fields (typically, nat.choose_eq_factorial_div_factorial, or bernoulli_poly). Instead of having results stated directly for char zero fields, we have results for ℚ that we then need to coerce. That seems to go against the idea of avoiding specificity, and more pragmatically it adds an annoying layer of coercion.
What should we do?

[Kevin Buzzard]

How about Q-algebras? When Ashvni and I were working on Bernoulli polynomials this was the generality we wanted (we wanted to apply these theorems in the power series ring $\mathbb{Q}[[T]]$ and had to keep coercing twice)

[Yaël Dillies]

Oooh, algebras aren't fields. That makes sense.
But my point still holds for the rest of the uses.

[Yaël Dillies]

But to be fair even then you should be able to replace ℚ by any char zero field. You just won't get rid of the algebra layer.

[Eric Wieser]

docs#rat.algebra_rat makes all char-zero division_rings Q-algebras, right?

[Eric Wieser]

Oh no, I'd missed that they have to be char 0 - so we can't just put an of_rat field in division_ring to solve the algebra diamonds

[Yaël Dillies]

I rather meant "Is there a use for these lemmas on α-algebras?"

[Yaël Dillies]

One counterpoint to my idea is that Lean has to figure out more stuff when applying a lemma.