no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
classical
refine' ⟨fun _ => ⟨le_total⟩, fun H => iff_dvd_total.mpr ⟨fun a b => _⟩⟩
have := @IsTotal.total _ _ H (Ideal.span {a}) (Ideal.span {b})
simp_rw [Ideal.span_singleton_le_span_singleton] at this
exact this.symm
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
⊢ a ∣ b ∨ b ∣ a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
refine' ⟨fun _ => ⟨le_total⟩, fun H => iff_dvd_total.mpr ⟨fun a b => _⟩⟩
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
⊢ a ∣ b ∨ b ∣ a
have := @IsTotal.total _ _ H (Ideal.span {a}) (Ideal.span {b})
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a
simp_rw [Ideal.span_singleton_le_span_singleton] at this
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.525453
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal (Ideal R) fun x x_1 => x ≤ x_1
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a
exact this.symm