Theorems · Definition · commutative algebra

ValuativeRel.RankLeOneStruct.casesOn

{R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] →
      {motive : ValuativeRel.RankLeOneStruct R → Sort u} →
        (t : ValuativeRel.RankLeOneStruct R) →
          ((emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal) →
              (strictMono : StrictMono ⇑emb) → motive { emb := emb, strictMono := strictMono }) →
            motive t

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringValuativeRel