Theorems · Definition · commutative algebra

RingNorm.mk.noConfusion

{R : Type u_2} →
  {inst : NonUnitalNonAssocRing R} →
    {P : Sort u} →
      {toRingSeminorm : RingSeminorm R} →
        {eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0} →
          {toRingSeminorm' : RingSeminorm R} →
            {eq_zero_of_map_eq_zero'' : ∀ (x : R), toRingSeminorm'.toFun x = 0 → x = 0} →
              { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
                  { toRingSeminorm := toRingSeminorm', eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'' } →
                (toRingSeminorm ≍ toRingSeminorm' → P) → P

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

1 results in Mathlib

Foundations

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