Theorems · Theorem · number theory

Projectivization.mulHeight_mk

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι] {x : ι → K}
  (hx : x ≠ 0), (Projectivization.mk K x hx).mulHeight = Height.mulHeight x

Defined in

Mathlib.NumberTheory.Height.Projectivization

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFinite