English
Under a MulEquiv, a DecompositionMonoid transfers primal decomposition.
Русский
Под действием MulEquiv декомпозиционный моноид переносит примальную декомпозицию.
LaTeX
$$$\text{DecompositionMonoid}(\alpha) \leftarrow_f \text{DecompositionMonoid}(\beta)$$$
Lean4
/-- If `G` is a `LeftCancelSemiGroup`, left multiplication by `g` yields an equivalence between `G`
and the set of elements of `G` divisible by `g`.
-/
protected noncomputable def dvd {G : Type*} [LeftCancelSemigroup G] (g : G) : G ≃ { a : G // g ∣ a }
where
toFun := fun a ↦ ⟨g * a, ⟨a, rfl⟩⟩
invFun := fun ⟨_, h⟩ ↦ h.choose
left_inv := fun _ ↦ by simp
right_inv := by
rintro ⟨_, ⟨_, rfl⟩⟩
simp
