Theorems · Definition · commutative algebra

ValuativeRel.RankLeOneStruct.mk.noConfusion

{R : Type u_1} →
  {inst : Semiring R} →
    {inst_1 : ValuativeRel R} →
      {P : Sort u} →
        {emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal} →
          {strictMono : StrictMono ⇑emb} →
            {emb' : ValuativeRel.ValueGroupWithZero R →*₀ NNReal} →
              {strictMono' : StrictMono ⇑emb'} →
                { emb := emb, strictMono := strictMono } = { emb := emb', strictMono := strictMono' } →
                  (emb ≍ emb' → P) → P

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

1 results in Mathlib

Foundations

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