noncomputable def morphismDegree (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain A] [Algebra B A] [FaithfulSMul B A] : ℕ

The degree of a finite morphism of integral domains, defined via the fraction-field extension [K(A) : K(B)].

theorem morphismDegree_eq_finrank (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain A] [Algebra B A] [FaithfulSMul B A] [Algebra.IsAlgebraic B A] : morphismDegree B A = Module.finrank B A

For an algebraic extension of domains, the fraction-field degree agrees with the module rank: [K(A) : K(B)] = rank_B A.