Theorems · Theorem · number theory

Height.mulHeight_fun_prod_eq

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u} [inst_2 : Fintype α]
  {ι : α → Type v} [∀ (a : α), Finite (ι a)] {x : (a : α) → ι a → K},
  (∀ (a : α), x a ≠ 0) → (Height.mulHeight fun I => ∏ a, x a (I a)) = ∏ a, Height.mulHeight (x a)

Consider a finite family x : (a : α) → ι a → K of tuples. Then the multiplicative height of the "multiplication table" fun (I : (a : α) → ι a ↦ ∏ a, x a (I a)) is the product of the multiplicative heights of all the x a.

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

1 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldHeight.AdmissibleAbsValuesFintypeFinite