Skip to content

Conversation

@YaelDillies
Copy link
Member

Not all integers appear as discriminants of a quadratic field.

Not all integers appear as discriminants of a quadratic field.
Comment on lines 43 to 44
/-- Fundamental discriminants are those integers `D` that appear as discriminants of quadratic
fields.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does mathlib not have the notion of a discriminant of a quadratic field?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure it does, but the notion of fundamental discriminant can be described very elementarily. That it corresponds to discriminants of quadratic fields is definitely something we should state, if that's what you mean

Copy link
Member

@Paul-Lez Paul-Lez Jan 21, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could be a nice category test or category undergradute statement!

@YaelDillies YaelDillies added WIP Work in progress awaiting-newer-lean Cannot be merged until the repo moves to a newer Lean version labels Jan 25, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-newer-lean Cannot be merged until the repo moves to a newer Lean version misformalization wikipedia WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants