Theorem finrank_quotient_span_eq_natDegree'

Modification history

2025-09-16 15:34
Mathlib/RingTheory/IsAdjoinRoot.lean
feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (#26101) …
Added finrank_quotient_span_eq_natDegree'View on Github →