Theorems · Theorem · commutative algebra

Valuation.Uniformizer.mk.injEq

∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] (val : ↥v.integer) (valuation_gt_one : v.IsUniformizer ↑val) (val_1 : ↥v.integer)
  (valuation_gt_one_1 : v.IsUniformizer ↑val_1),
  ({ val := val, valuation_gt_one := valuation_gt_one } = { val := val_1, valuation_gt_one := valuation_gt_one_1 }) =
    (val = val_1)

Defined in

Mathlib.RingTheory.Valuation.Discrete.Basic

Cited by

0 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroRingValuation.IsRankOneDiscrete