English
There exists a Galois coinsertion between Subgroup.ofUnits and Submonoid.units, linking reduction and coercion between units.
Русский
Существует coinsertion Галуа между Subgroup.ofUnits и Submonoid.units, устанавливающее связь снижения и включения единиц.
LaTeX
$$GaloisCoinsertion(Subgroup.ofUnits, Submonoid.units)$$
Lean4
/-- A Galois coinsertion exists between the coercion from a subgroup of units to a submonoid and
the reduction from a submonoid to its unit group. -/
@[to_additive /-- A Galois coinsertion exists between the coercion from a additive subgroup of
additive units to a additive submonoid and the reduction from a additive submonoid to its unit
group. -/
]
def ofUnits_units_gci : GaloisCoinsertion (Subgroup.ofUnits (M := M)) (Submonoid.units) :=
GaloisCoinsertion.monotoneIntro Submonoid.units_mono Subgroup.ofUnits_mono Submonoid.ofUnits_units_le
Subgroup.units_ofUnits_eq
