Theorems · Theorem · commutative algebra

MulRingNorm.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

NonAssocRing