Theorems · Definition · commutative algebra

MulRingSeminorm.casesOn

{R : Type u_2} →
  [inst : NonAssocRing R] →
    {motive : MulRingSeminorm R → Sort u} →
      (t : MulRingSeminorm 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) →
                motive { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' }) →
          motive t

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocRing