Theorems · Definition · commutative algebra

MulRingSeminorm.mk.noConfusion

{R : Type u_2} →
  {inst : NonAssocRing R} →
    {P : Sort u} →
      {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' : AddGroupSeminorm R} →
              {map_one'' : toAddGroupSeminorm'.toFun 1 = 1} →
                {map_mul'' :
                    ∀ (x y : R),
                      toAddGroupSeminorm'.toFun (x * y) = toAddGroupSeminorm'.toFun x * toAddGroupSeminorm'.toFun y} →
                  { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' } =
                      { toAddGroupSeminorm := toAddGroupSeminorm', map_one' := map_one'', map_mul' := map_mul'' } →
                    (toAddGroupSeminorm ≍ toAddGroupSeminorm' → P) → P

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

1 results in Mathlib

Foundations

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