uniqueFactorizationMonoid — Mathlib

English

If an isomorphism e preserves multiplication, then UFMonoid property is transferred to the target.

Русский

Если биекция сохраняет умножение, то свойство уникальной факторизации переносится на целевой множитель.

LaTeX

$$$\text{If } e: \alpha \to \beta^{\times}\text{ is a multiplicative equivalence and } \alpha\text{ is UFMonoid, then } \beta\text{ is UFMonoid.}$$$

Lean4

theorem uniqueFactorizationMonoid (e : α ≃* β) (hα : UniqueFactorizationMonoid α) : UniqueFactorizationMonoid β :=
  by
  rw [UniqueFactorizationMonoid.iff_exists_prime_factors] at hα ⊢
  intro a ha
  obtain ⟨w, hp, u, h⟩ :=
    hα (e.symm a) fun h =>
      ha <| by
        convert ← map_zero e
        simp [← h]
  exact
    ⟨w.map e, fun b hb =>
      let ⟨c, hc, he⟩ := Multiset.mem_map.1 hb
      he ▸ (prime_iff e).2 (hp c hc),
      Units.map e.toMonoidHom u, by
      rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h, apply_symm_apply]⟩

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