Theorems · Theorem · functional analysis

AbsoluteValue.LiesOver.comp_eq

∀ {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) [self : w.LiesOver v], w.comp ⋯ = v

Defined in

Mathlib.Analysis.Normed.Ring.WithAbs

Cited by

4 results in Mathlib

Foundations

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

Assumes

AbsoluteValue.LiesOver