Theorems · Theorem · commutative algebra

ValuativeExtension.vle_iff_vle

∀ {A : Type u_1} {B : Type u_2} {inst : CommSemiring A} {inst_1 : Semiring B} {inst_2 : ValuativeRel A}
  {inst_3 : ValuativeRel B} {inst_4 : Algebra A B} [self : ValuativeExtension A B] (a b : A),
  (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

ValuativeExtension