isPrimal_mk — Mathlib

English

For any a in M, the primality of the associate class [a] is equivalent to the primality of a.

Русский

Для любого a в M примитивность класса ассоциированности [a] эквивалентна примитивности самого элемента a.

LaTeX

$$$ \text{IsPrimal}([a]) \iff \text{IsPrimal}(a) $$$

Lean4

@[simp]
theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a :=
  by
  simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]
  constructor <;> intro h b c dvd <;> obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
  · obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
    exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
  · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩

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