Field rank nonzero

Stream: Is there code for X?

[Artie Khovanov]

Is there a theorem which says that Module.finrank K L ≠ 0 for [Field K] [Field L] [Algebra K L] [Module.Finite K L]?

[Weiyi Wang]

does docs#Module.finrank_eq_zero_iff_of_free docs#Module.finrank_pos_iff_of_free help?

[Artie Khovanov]

Oh it's just Module.finrank_pos oops