divMonoidHom — Mathlib

English

For DivisionComMonoid α, the map (a,b) ↦ a/b from α × α to α is a monoid homomorphism.

Русский

Для DivisionComMonoid α отображение (a,b) ↦ a/b из α × α в α является моноид-гомоморфизмом.

LaTeX

$$$\\text{divMonoidHom}: \\alpha \\times \\alpha \\to^* \\alpha\\quad (a,b) \\mapsto a/b$$$

Lean4

/-- Division as a monoid homomorphism. -/
@[to_additive (attr := simps) /-- Subtraction as an additive monoid homomorphism. -/
    ]
def divMonoidHom [DivisionCommMonoid α] : α × α →* α
    where
  toFun a := a.1 / a.2
  map_one' := div_one _
  map_mul' _ _ := mul_div_mul_comm _ _ _ _

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