English
The inl construction is defined via a unit-coercion into the product of units, followed by a lift to WithZero.
Русский
Конструкция inl задаётся через единичный коэффициент в произведении единиц и последующий подъём в WithZero.
LaTeX
$$$\text{inl} \; = \; (\text{WithZero.map'} (\\text{.inl} \, _ \, _)) \circ (\\text{MonoidWithZeroHomClass.toMonoidWithZeroHom} \, \, \,)$$$
Lean4
/-- Given groups with zero `G₀`, `H₀`, the natural inclusion ordered homomorphism from
`H₀` to `WithZero (G₀ˣ × H₀ˣ)`, which is the group with zero that can be identified
as their product. -/
def inr [DecidablePred fun x : H₀ ↦ x = 0] : H₀ →*₀ WithZero (G₀ˣ × H₀ˣ) :=
(WithZero.map' (.inr _ _)).comp (MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv.symm)
