isIntegral — Mathlib

English

If G is finite and A ⊆ B with IsInvariant A B G, then B is integral over A.

Русский

Если G конечна и B инвариантен над A, то B интегрально над A.

LaTeX

$$$[Finite G] \Rightarrow (\text{Algebra.IsInvariant } A B G) \Rightarrow \text{Algebra.IsIntegral } A B$$$

Lean4

theorem isIntegral [Finite G] : Algebra.IsIntegral A B :=
  by
  cases nonempty_fintype G
  refine ⟨fun b ↦ ?_⟩
  obtain ⟨p, hp1, -, hp2⟩ :=
    Polynomial.lifts_and_natDegree_eq_and_monic (charpoly_mem_lifts A B G b) (monic_charpoly G b)
  exact ⟨p, hp2, by rw [← eval_map, hp1, eval_charpoly]⟩

Похожие утверждения