English
If f is a MulEquiv between semigroups and β is a DecompositionMonoid, then α is a DecompositionMonoid with a primal decomposition via f.
Русский
Если f—MulEquiv между полугруппами, а β — декомпозиционный моноид, то α становится декомпозиционным моноидом с примальной декомпозицией через f.
LaTeX
$$$DecompositionMonoid(\alpha) \text{ given } f: (\alpha \simeq_* \beta) \text{ and } DecompositionMonoid(\beta)$$$
Lean4
theorem decompositionMonoid (f : F) [DecompositionMonoid β] : DecompositionMonoid α where
primal a b c
h := by
rw [← map_dvd_iff f, map_mul] at h
obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h
refine ⟨symm f a₁, symm f a₂, ?_⟩
simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply]
iterate 2 erw [(f : α ≃* β).apply_symm_apply]
exact h
