Theorems · Theorem · commutative algebra

MulRingSeminorm.mk.injEq

∀ {R : Type u_2} [inst : NonAssocRing R] (toAddGroupSeminorm : AddGroupSeminorm R)
  (map_one' : toAddGroupSeminorm.toFun 1 = 1)
  (map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
  (toAddGroupSeminorm_1 : AddGroupSeminorm R) (map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1)
  (map_mul'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) = toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y),
  ({ toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toAddGroupSeminorm = toAddGroupSeminorm_1)

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocRing