Theorems · Definition · functional analysis

AbsoluteValue.LiesOver.casesOn

{K : Type u_3} →
  {L : Type u_4} →
    {S : Type u_5} →
      [inst : CommRing K] →
        [inst_1 : IsSimpleRing K] →
          [inst_2 : CommRing L] →
            [inst_3 : Algebra K L] →
              [inst_4 : PartialOrder S] →
                [inst_5 : Nontrivial L] →
                  [inst_6 : Semiring S] →
                    {w : AbsoluteValue L S} →
                      {v : AbsoluteValue K S} →
                        {motive : w.LiesOver v → Sort u} →
                          (t : w.LiesOver v) → ((comp_eq : w.comp ⋯ = v) → motive ⋯) → motive t

Defined in

Mathlib.Analysis.Normed.Ring.WithAbs

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Quot.sound

Assumes

CommRingIsSimpleRingCommRingAlgebraPartialOrderNontrivialSemiring