Theorems · Theorem · commutative algebra
Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial
∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
[inst_2 : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup]
[inst_3 : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup], ∃ π, v.IsUniformizer ↑π- Cited by
- 2 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- SetLike.coeproof · cited by 8,199
- Fieldstatement and proof · cited by 7,404
- Set.imageproof · cited by 5,609
- Set.rangeproof · cited by 4,705
- Subgroupstatement · cited by 3,593
- Unitsstatement and proof · cited by 2,804
- Nontrivialstatement and proof · cited by 2,416
- Units.valproof · cited by 1,966
- le_of_ltproof · cited by 1,175
- Valuationstatement and proof · cited by 823
Cited by2
Results whose statement or proof uses this declaration.
- Valuation.valuationSubring_not_isFieldproof · cited by 1
- Valuation.isUniformizer_of_maximalIdeal_eq_spanproof · cited by 0