English
For a Dedekind domain A, and ideals I, element x ∈ A, and natural n, the n-th power of I is less than or equal to the principal ideal generated by x iff x ∈ I^n.
Русский
В Дедекдиновой области A для идеала I, элемента x ∈ A и натурального n верно: I^n ≤ (x) тогда и только если x ∈ I^n.
LaTeX
$$I^n ≤ (x) ⇔ x ∈ I^n$$
Lean4
@[simp]
theorem sup_mul_inf (I J : Ideal A) : (I ⊔ J) * (I ⊓ J) = I * J :=
by
letI := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
have hgcd : gcd I J = I ⊔ J := by
rw [gcd_eq_normalize _ _, normalize_eq]
· rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩
· rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]
simp
have hlcm : lcm I J = I ⊓ J := by
rw [lcm_eq_normalize _ _, normalize_eq]
· rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]
simp
· rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩
rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]
