Theorems · Theorem · commutative algebra

RingNorm.mk.inj

∀ {R : Type u_2} {inst : NonUnitalNonAssocRing R} {toRingSeminorm : RingSeminorm R}
  {eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0} {toRingSeminorm_1 : RingSeminorm R}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0},
  { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toRingSeminorm = toRingSeminorm_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