show · nf.degree_mathlib_def all knowls · up · search:

This is also defined in mathlib as finrank ℚ K, where $K$ is the number field and finrank is its module rank over the rationals.

Authors:
Knowl status:
  • Review status: beta
  • Last edited by Chris Birkbeck on 2025-10-23 15:50:56
Referred to by:

Not referenced anywhere at the moment.

History: (expand/hide all)