toMonoidWithZeroHom_withZeroUnitsEquiv

English

There is a canonical monoid-with-zero hom from a group G₀ to WithZero (G₀ˣ × H₀ˣ) obtained by embedding into units and using the WithZero equivalence; this map coincides with a standard lift.

Русский

Существует каноническое моноидальное с нулём отображение из G₀ в WithZero (G₀ˣ × H₀ˣ), получаемое внедрением в единицы и использованием эквивалентности WithZero; это отображение совпадает с обычным возвышением.

LaTeX

$$$\text{MonoidWithZeroHom} \bigl(G_0, WithZero (G_0^\times \times H_0^\times)\bigr) = WithZero.lift' (Units.coeHom G_0)$$$

Lean4

@[simp]
theorem toMonoidWithZeroHom_withZeroUnitsEquiv [GroupWithZero M₀] [DecidablePred fun x : M₀ ↦ x = 0] :
    MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv = WithZero.lift' (Units.coeHom M₀) :=
  rfl

Похожие утверждения