Uniqueness of power-multiplicative norms

In this file, we prove uniqueness of power-multiplicative norms over complete normed fields.

Main Results

• IsPowMul.unique : uniqueness of power-multiplicative norms over complete normed fields.

theorem IsPowMul.unique {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] {f g : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hg_pm : IsPowMul ⇑g) : f = g

Uniqueness of power-multiplicative norms over complete normed fields.

theorem MulAlgebraNorm.unique {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] (f g : MulAlgebraNorm K L) : f = g

Uniqueness of multiplicative algebra norms over complete normed fields.

def AlgebraNorm.toMulAlgebraNorm {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] (f : AlgebraNorm K L) (hf : IsPowMul ⇑f) : MulAlgebraNorm K L

A power-multiplicative algebra norm over a complete normed field is multiplicative.

Equations

• f.toMulAlgebraNorm hf = { toAddGroupSeminorm := f.toAddGroupSeminorm, map_one' := ⋯, map_mul' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }

@[simp]

theorem AlgebraNorm.coe_toMulAlgebraNorm {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] (f : AlgebraNorm K L) (hf : IsPowMul ⇑f) : ⇑(f.toMulAlgebraNorm hf) = ⇑f

@[simp]

theorem AlgebraNorm.toAlgebraNorm_toMulAlgebraNorm {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] (f : AlgebraNorm K L) (hf : IsPowMul ⇑f) : (f.toMulAlgebraNorm hf).toAlgebraNorm = f