divMonoidWithZeroHom — Mathlib

English

For any MonoidWithZeroHom f, composing with the constant-1 hom preserves the constant-1 behavior: 1 ∘ f = 1.

Русский

Для любого MonoidWithZeroHom f композиция 1 с f сохраняет константно-единичное отображение: 1 ∘ f = 1.

LaTeX

$$$(1 : N \to*₀ G) \circ f = (1 : M \to*₀ G)$$$

Lean4

/-- Division as a multiplicative homomorphism with zero. -/
@[simps]
def divMonoidWithZeroHom [CommGroupWithZero M₀] : M₀ × M₀ →*₀ M₀
    where
  __ := divMonoidHom
  map_zero' := zero_div _

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