Theorems · Theorem · commutative algebra

MulRingNorm.mk.inj

∀ {R : Type u_2} {inst : NonAssocRing R} {toMulRingSeminorm : MulRingSeminorm R}
  {eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0} {toMulRingSeminorm_1 : MulRingSeminorm R}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0},
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toMulRingSeminorm = toMulRingSeminorm_1

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

1 results in Mathlib

Foundations

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