Theorems · Theorem · functional analysis

MulAlgebraNorm.mk.inj

∀ {R : Type u_1} {inst : SeminormedCommRing R} {S : Type u_2} {inst_1 : Ring S} {inst_2 : Algebra R S}
  {toMulRingNorm : MulRingNorm S} {smul' : ∀ (a : R) (x : S), toMulRingNorm.toFun (a • x) = ‖a‖ * toMulRingNorm.toFun x}
  {toMulRingNorm_1 : MulRingNorm S}
  {smul'_1 : ∀ (a : R) (x : S), toMulRingNorm_1.toFun (a • x) = ‖a‖ * toMulRingNorm_1.toFun x},
  { toMulRingNorm := toMulRingNorm, smul' := smul' } = { toMulRingNorm := toMulRingNorm_1, smul' := smul'_1 } →
    toMulRingNorm = toMulRingNorm_1

Defined in

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Cited by

1 results in Mathlib

Foundations

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