Mathlib Map

Theorems · Theorem · commutative algebra

PreTilt.valAux_add

∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] (f g : PreTilt O p),
      PreTilt.valAux K v O p (f + g) ≤ max (PreTilt.valAux K v O p f) (PreTilt.valAux K v O p g)
Defined in
Mathlib.RingTheory.Perfection
Cited by
0 results in Mathlib
Foundations
Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldCommRingAlgebraFactFact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PreTilt.val · cited by 3PreTilt.valDFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraField · cited by 7404FieldNNReal · cited by 4310NNRealFact · cited by 2726Factadd_zero · cited by 2707add_zerozero_add · cited by 2366zero_addNat.Prime · cited by 2059Nat.PrimeIsUnit · cited by 1602IsUniteq_or_ne · cited by 1117eq_or_nele_trans · cited by 985le_transmap_add · cited by 964map_addValuation · cited by 823Valuationsup_of_le_left · cited by 218sup_of_le_leftPreTilt.valAux_addCITED BYCITES

Cites35

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coeproof · cited by 62,936
  • CommRingstatement and proof · cited by 17,173
  • Algebrastatement and proof · cited by 11,388
  • Fieldstatement and proof · cited by 7,404
  • NNRealstatement and proof · cited by 4,310
  • Factstatement and proof · cited by 2,726
  • add_zeroproof · cited by 2,707
  • zero_addproof · cited by 2,366
  • Nat.Primestatement and proof · cited by 2,059
  • IsUnitstatement and proof · cited by 1,602
  • eq_or_neproof · cited by 1,117
  • le_transproof · cited by 985

Cited by1

Results whose statement or proof uses this declaration.