English
There is a natural multiplicative equivalence between the group of units of a monoid M and the submonoid of unit elements in M.
Русский
Существует естественное мультипликативное эквивалентность между группой единиц моноя M и подмoноидом единиц в M.
LaTeX
$$$ Units(M) \cong IsUnit.submonoid M $$$
Lean4
/-- The multiplicative equivalence between the type of units of `M` and the submonoid of unit
elements of `M`. -/
@[to_additive (attr := simps!) /-- The additive equivalence between the type of additive units of
`M` and the additive submonoid whose elements are the additive units of `M`. -/
]
noncomputable def unitsTypeEquivIsUnitSubmonoid [Monoid M] : Mˣ ≃* IsUnit.submonoid M
where
toFun x := ⟨x, Units.isUnit x⟩
invFun x := x.prop.unit
left_inv _ := IsUnit.unit_of_val_units _
right_inv x := by simp_rw [IsUnit.unit_spec]
map_mul' x y := by simp_rw [Units.val_mul]; rfl
