discrete_field vs field

Stream: new members

[Kenny Lau]

Is the idiom to not use field at all?

[Johan Commelin]

Yes, I think that is what @Mario Carneiro said at some point. "Mathematicians should only use discrete_field."

[Kenny Lau]

ok thanks

[Kenny Lau]

that would certainly make things longer

[Kenny Lau]

can we petition to rename it dfield?

[Kenny Lau]

oh nvm it is in core

[Mario Carneiro]

I would petition to name it field :P

[Patrick Massot]

Please, don't feed the trolls...