Theorems · Theorem · commutative algebra

Valuation.HasExtension.val_isEquiv_comap

∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} {inst : CommRing R} {inst_1 : Ring A}
  {inst_2 : LinearOrderedCommMonoidWithZero ΓR} {inst_3 : LinearOrderedCommMonoidWithZero ΓA} {inst_4 : Algebra R A}
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [self : vR.HasExtension vA],
  vR.IsEquiv (Valuation.comap (algebraMap R A) vA)

The valuation vR on R is equivalent to the comap of the valuation vA on A

Defined in: Mathlib.RingTheory.Valuation.Extension
Cited by: 2 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Valuation.HasExtension

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Ringstatement and proof · cited by 7,463
Algebra.algebraMapstatement · cited by 4,706
Valuationstatement and proof · cited by 823
LinearOrderedCommMonoidWithZerostatement and proof · cited by 139
Valuation.IsEquivstatement · cited by 67
Valuation.HasExtensionstatement and proof · cited by 17
Valuation.comapstatement · cited by 15

Cited by2

Results whose statement or proof uses this declaration.

Valuation.HasExtension.val_map_le_iffproof · cited by 5
Valuation.HasExtension.val_map_eq_iffproof · cited by 0