English
If K,L,E are fields with K ≤ L ≤ E and L/K finite, then discr(K, pb.basis) is integral over K when pb.basis is a basis for L over K and E is algebraically closed.
Русский
Пусть K,L,E — поля, где K ⊆ L ⊆ E, а L/K является конечным. Тогда дискриминант дискр(K, pb.basis) интеграл над K, когда pb.basis образует базис L над K, а E алгебраически замкнуто.
LaTeX
$$$$ \\mathrm{IsIntegral}_K(\\mathrm{discr}\\,K\\,pb.basis) $$$$
Lean4
/-- If `K` and `L` are fields and `IsScalarTower R K L`, and `b : ι → L` satisfies
` ∀ i, IsIntegral R (b i)`, then `IsIntegral R (discr K b)`. -/
theorem discr_isIntegral {b : ι → L} (h : ∀ i, IsIntegral R (b i)) : IsIntegral R (discr K b) := by
classical
rw [discr_def]
exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))
