R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
⊢ (I ⊔ J) * (I ⊓ J) = I * J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
⊢ (I ⊔ J) * (I ⊓ J) = I * J
letI := Classical.decEq (Ideal A)
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
⊢ (I ⊔ J) * (I ⊓ J) = I * J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
⊢ (I ⊔ J) * (I ⊓ J) = I * J
letI := Classical.decEq (Associates (Ideal A))
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ (I ⊔ J) * (I ⊓ J) = I * J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
⊢ (I ⊔ J) * (I ⊓ J) = I * J
letI := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
no goals
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
hlcm : lcm I J = I ⊓ J
⊢ (I ⊔ J) * (I ⊓ J) = I * J
rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ⊔ J ∣ gcd I J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J = I ⊔ J
rw [gcd_eq_normalize _ _, normalize_eq]
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J
rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
no goals
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ⊔ J ∣ gcd I J
rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]
no goals
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J
simp
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J ∣ I ⊓ J

R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J = I ⊓ J
rw [lcm_eq_normalize _ _, normalize_eq]
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J ∣ I ⊓ J
rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]
no goals
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J
simp
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J
rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
no goals
R : Type ?u.886660
A : Type u_1
K : Type ?u.886666
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : Ideal A
this✝¹ : DecidableEq (Ideal A) := Classical.decEq (Ideal A)
this✝ : DecidableEq (Associates (Ideal A)) := Classical.decEq (Associates (Ideal A))
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩