regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv

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]

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