Theorems · Theorem · functional analysis

AlgebraNorm.mk.inj

∀ {R : Type u_1} {inst : SeminormedCommRing R} {S : Type u_2} {inst_1 : Ring S} {inst_2 : Algebra R S}
  {toRingNorm : RingNorm S} {smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x}
  {toRingNorm_1 : RingNorm S} {smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x},
  { toRingNorm := toRingNorm, smul' := smul' } = { toRingNorm := toRingNorm_1, smul' := smul'_1 } →
    toRingNorm = toRingNorm_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