NormFormula.lean

theorem normFormula_real_natPow_rpow_inv_mul_cancel
    {a : ℝ} (ha : 0 ≤ a) {m n : ℕ} (hm : 0 < m) (hn : 0 < n) :
    (a ^ n) ^ (1 / ((m * n : ℕ) : ℝ)) = a ^ (1 / (m : ℝ))

theorem normFormula_finiteExtensionNormFormulaValue_eq_minpoly_coeff_zero_rpow
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    finiteExtensionNormFormulaValue v x =
      v ((minpoly K x).coeff 0) ^
        (1 / ((minpoly K x).natDegree : ℝ))

theorem normFormula_finiteExtensionNormFormulaValue_algebraMap
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (a : K) :
    finiteExtensionNormFormulaValue v (algebraMap K L a) = v a

theorem normFormula_finiteExtensionNormFormulaValue_pow_finrank_eq_norm
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    finiteExtensionNormFormulaValue v x ^ Module.finrank K L =
      v (Algebra.norm K x)

theorem normFormula_finiteExtensionNormFormulaValue_eq_zero_iff
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    finiteExtensionNormFormulaValue v x = 0 ↔ x = 0

theorem normFormula_finiteExtensionNormFormulaValue_mul
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x y : L) :
    finiteExtensionNormFormulaValue v (x * y) =
      finiteExtensionNormFormulaValue v x *
        finiteExtensionNormFormulaValue v y

theorem normFormula_finiteExtensionNormFormulaValue_inv
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    finiteExtensionNormFormulaValue v x⁻¹ =
      (finiteExtensionNormFormulaValue v x)⁻¹

theorem normFormula_finiteExtensionNormFormulaValue_div
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x y : L) :
    finiteExtensionNormFormulaValue v (x / y) =
      finiteExtensionNormFormulaValue v x /
        finiteExtensionNormFormulaValue v y

theorem normFormula_finiteExtensionNormFormulaValue_le_one_iff_minpoly_coeff_zero_le_one
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    finiteExtensionNormFormulaValue v x ≤ 1 ↔
      v ((minpoly K x).coeff 0) ≤ 1

theorem normFormula_finiteExtensionNormFormulaValue_le_one_of_isIntegral
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {x : L}
    (hx : IsIntegral
      (absoluteValueValuationSubring v hnonarch) x) :
    finiteExtensionNormFormulaValue v x ≤ 1

theorem comap_to_middle_hasExtension_of_top_hasExtension
    {M : Type y} [Field M] [Algebra L M] [Algebra K M]
    [IsScalarTower K L M]
    {ΓM : Type z} [LinearOrderedCommGroupWithZero ΓM]
    (vK : _root_.Valuation K ΓK) (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vM] :
    vK.HasExtension (vM.comap (algebraMap L M))