English
Under the stated hypotheses, the set of A-algebra automorphisms of B is finite, hence B ≃_A B has finite cardinality.
Русский
При данных предпосылках множество A-алгебраических автоморфизмов B конечносано, следовательно B ≃_A B конечно по кардинальности.
LaTeX
$$$[IsDomain A] \\to [IsDomain B] \\to [IsIntegrallyClosed B] \\to [Module.Finite A B] \\to [NoZeroSMulDivisors A B] \\Rightarrow Fintype (AlgEquiv A B B)$$$
Lean4
/-- The restriction of the norm on `L/K` restricted onto `B/A` in an AKLB setup.
See `Algebra.intNorm` instead. -/
noncomputable def intNormAux : B →* A
where
toFun := fun s ↦
IsIntegralClosure.mk' (R := A) A (Algebra.norm K (algebraMap B L s))
(isIntegral_norm K <| IsIntegral.map (IsScalarTower.toAlgHom A B L) (IsIntegralClosure.isIntegral A L s))
map_one' := by simp
map_mul' := fun x y ↦ by simpa using IsIntegralClosure.mk'_mul _ _ _ _ _
