English
Let x be an element in the real embedding space of a number field K. Then the product over all places w of the quantity expMapBasis(x) at w, raised to the power w.mult, equals exp(x at w0) raised to the degree of K over ℚ.
Русский
Пусть x лежит в пространстве действительных вложений числа поля K. Тогда произведение по всем местам w от expMapBasis(x) на месте w, возведённое в степень w.mult, равно exp(x по месту w0) в степени finrankℚ K.
LaTeX
$$$\displaystyle \prod_w (\expMapBasis(x)_w)^{w.mult} = \left( e^{x_{w_0}} \right)^{\operatorname{finrank}_{\mathbb{Q}} K}$$$
Lean4
theorem prod_expMapBasis_pow (x : realSpace K) :
∏ w, (expMapBasis x w) ^ w.mult = Real.exp (x w₀) ^ Module.finrank ℚ K :=
by
simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib, prod_pow_eq_pow_sum, sum_mult_eq, ←
prod_pow]
rw [prod_comm]
simp_rw [Real.rpow_pow_comm (apply_nonneg _ _), Real.finset_prod_rpow _ _ fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _,
prod_eq_abs_norm, Units.norm, Rat.cast_one, Real.one_rpow, prod_const_one, mul_one]
