English
The canonical equivalence between a submonoid H and its opposite composes correctly with the membership equivalence.
Русский
Каноническое эквивалентное отображение между подмонодом H и его противоположностью корректно грамотно сочетается с эквивалентностью принадлежности.
LaTeX
$$$ H \equiv H^{op} \quad \text{and} \quad (\text{membership correspondence}) $$$$
Lean4
/-- Additive submonoids of an additive monoid `A` are isomorphic to
multiplicative submonoids of `Multiplicative A`. -/
@[simps]
def toSubmonoid : AddSubmonoid A ≃o Submonoid (Multiplicative A)
where
toFun
S :=
{ carrier := Multiplicative.toAdd ⁻¹' S
one_mem' := S.zero_mem'
mul_mem' := fun ha hb => S.add_mem' ha hb }
invFun
S :=
{ carrier := Multiplicative.ofAdd ⁻¹' S
zero_mem' := S.one_mem'
add_mem' := fun ha hb => S.mul_mem' ha hb }
left_inv x := by cases x; rfl
right_inv x := by cases x; rfl
map_rel_iff' := Iff.rfl
