Theorems · Theorem · commutative algebra

MulRingSeminorm.mk.inj

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

1 results in Mathlib

Foundations

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