English
If there are only finitely many maximal ideals in a Dedekind domain, then every invertible fractional ideal is principal.
Русский
Если в Дедекинд домене конечное число максимальных идеалов, то каждый обратимый дробный идеал является порожденным (principal).
LaTeX
$$$$\\text{IsPrincipalIdealRing}(R)$$$$
Lean4
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
and `L` has no zero smul divisors by `A`, the `A`-rank of the integral closure `C` of `A` in `L`
is equal to the `K`-rank of `L`. -/
theorem rank [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L] : Module.finrank A C = Module.finrank K L :=
by
haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := IsIntegralClosure.isLocalization A K L C
let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b]
