noncomputable def tracePairing (A : Type u_1) [CommRing A] (B : Type u_2) [CommRing B] [Algebra A B] : LinearMap.BilinForm A B

theorem prop_5_17_isFractionRing (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra B L] [IsIntegralClosure B A L] [Algebra A B] [IsScalarTower A B L] : IsFractionRing B L

theorem prop_5_18_norm_isIntegral (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [Algebra B L] [IsIntegralClosure B A L] [Algebra A B] [IsScalarTower A B L] (b : B) : IsIntegral A ((Algebra.norm K) ((algebraMap B L) b))

theorem prop_5_18_trace_isIntegral (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [Algebra B L] [IsIntegralClosure B A L] [Algebra A B] [IsScalarTower A B L] (b : B) : IsIntegral A ((Algebra.trace K L) ((algebraMap B L) b))

theorem thm_5_20_traceForm_symmetric (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra K L] : (Algebra.traceForm K L).IsSymm

theorem thm_5_20_nondegenerate_of_separable (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : (Algebra.traceForm K L).Nondegenerate

theorem thm_5_20_separable_of_nondegenerate (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hnd : (Algebra.traceForm K L).Nondegenerate) : Algebra.IsSeparable K L

theorem thm_5_20_nondegenerate_iff_separable (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] : [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (Algebra.traceForm K L).Nondegenerate].TFAE

theorem prop_5_22_finite (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [Algebra B L] [IsIntegralClosure B A L] [Algebra A B] [IsScalarTower A B L] [IsDedekindDomain A] [Algebra.IsSeparable K L] : Module.Finite A B

theorem prop_5_22_isNoetherian (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [Algebra B L] [IsIntegralClosure B A L] [Algebra A B] [IsScalarTower A B L] [IsDedekindDomain A] [Algebra.IsSeparable K L] : IsNoetherian A B

theorem traceForm_symmetric (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra K L] : (Algebra.traceForm K L).IsSymm

Alias of thm_5_20_traceForm_symmetric.