English
In a CM-field K, the ratio regulator(K) / regulator(K^+) equals 2^{rank(K)} times the reciprocal of indexRealUnits(K); i.e., regulator(K) / regulator(K^+) = 2^{rank(K)} · (indexRealUnits(K))^{-1}.
Русский
Для поля CM K отношение регулятора regulator(K) к regulator(K^+) равно 2^{rank(K)} умножить на обратную величину indexRealUnits(K).
LaTeX
$$$\\dfrac{\\mathrm{regulator}(K)}{\\mathrm{regulator}(K^+)} = 2^{\\mathrm{rank}(K)} \\cdot (\\mathrm{indexRealUnits}(K))^{-1}$$$
Lean4
theorem regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv :
regulator K / regulator K⁺ = 2 ^ rank K * (indexRealUnits K : ℝ)⁻¹ := by
rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator (realFundSystem K),
regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm, div_self (by positivity), one_mul]