theorem SepClosedDecomposition.algHom_card_eq_finrank_of_isSepClosed (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : Fintype.card (L →ₐ[K] Ω) = Module.finrank K L

def SepClosedDecomposition.evalAlgHom (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] : L →ₐ[K] (L →ₐ[K] Ω) → Ω

def SepClosedDecomposition.tensorSepClosedAlgHom (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] : TensorProduct K Ω L →ₐ[Ω] (L →ₐ[K] Ω) → Ω

theorem SepClosedDecomposition.algHom_linearIndependent (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : LinearIndependent Ω fun (σ : L →ₐ[K] Ω) (l : L) => σ l

theorem SepClosedDecomposition.column_functions_linearIndependent (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : LinearIndependent Ω fun (i : Fin (Module.finrank K L)) (φ : L →ₐ[K] Ω) => φ ((Module.finBasis K L) i)

theorem SepClosedDecomposition.tensorSepClosedAlgHom_injective (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : Function.Injective ⇑(tensorSepClosedAlgHom K L Ω)

theorem SepClosedDecomposition.finrank_tensor_eq_finrank_pi_of_isSepClosed (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : Module.finrank Ω (TensorProduct K Ω L) = Module.finrank Ω ((L →ₐ[K] Ω) → Ω)

theorem SepClosedDecomposition.tensorSepClosedAlgHom_surjective (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : Function.Surjective ⇑(tensorSepClosedAlgHom K L Ω)

theorem SepClosedDecomposition.tensorSepClosedAlgHom_bijective (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : Function.Bijective ⇑(tensorSepClosedAlgHom K L Ω)

noncomputable def SepClosedDecomposition.tensorSepClosedAlgEquiv (K : Type u_1) (L : Type u_2) (Ω : Type u_3) [Field K] [Field L] [Field Ω] [Algebra K L] [Algebra K Ω] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsSepClosed Ω] : TensorProduct K Ω L ≃ₐ[Ω] (L →ₐ[K] Ω) → Ω