English
If A is a domain, B is integrally closed, B is finite over A, and NoZeroSMulDivisors holds, then the A-automorphism group of B is finite.
Русский
Если A — домен, B интегрально замкнутый, B конечно как модуль над A и выполнено условие NoZeroSMulDivisors, то группа A-автоморфизмов B конечна.
LaTeX
$$$[\\text{IsDomain } A]\\ [\\text{IsDomain } B]\\ [\\text{IsIntegrallyClosed } B]\\ [\\text{Module.Finite } A B]\\ [\\text{NoZeroSMulDivisors } A B]\\;\\Rightarrow\\; Fintype\\,(B \\simeq_A B)$$$
Lean4
noncomputable instance (priority := 900) [IsDomain A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B]
[NoZeroSMulDivisors A B] : Fintype (B ≃ₐ[A] B) :=
haveI : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
haveI : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) (FractionRing B) :=
IsIntegralClosure.isLocalization _ (FractionRing A) _ _
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
Fintype.ofEquiv _ (galRestrict A (FractionRing A) (FractionRing B) B).toEquiv
