squarefree_span_singleton — Mathlib

English

For a Dedekind domain with principal ideals, the span of a singleton is squarefree iff a is squarefree.

Русский

В кольце Дедекиндова, у которого все идеалы главные, спан от одного элемента квадратно свободен тогда и только тогда, когда сам элемент квадратно свободен.

LaTeX

$$Squarefree (span{a}) ⇔ Squarefree a$$

Lean4

@[simp]
theorem squarefree_span_singleton {a : R} : Squarefree (span { a }) ↔ Squarefree a :=
  by
  refine ⟨fun h x hx ↦ ?_, fun h I hI ↦ ?_⟩
  · rw [← span_singleton_dvd_span_singleton_iff_dvd, ← span_singleton_mul_span_singleton] at hx
    simpa using h _ hx
  · rw [← span_singleton_generator I, span_singleton_mul_span_singleton,
      span_singleton_dvd_span_singleton_iff_dvd] at hI
    exact isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)

Похожие утверждения