mul — Mathlib

English

A dot-notation alias for the inverse of a product: If a,b are invertible, then a*b is invertible with inverse inv(b) * inv(a).

Русский

Алиас в точке для произведения: если a,b обратимы, то a*b обратимо, и его обратное равно inv(b) * inv(a).

LaTeX

$$$\\text{Invertible}(a) \\land \\text{Invertible}(b) \\Rightarrow \\text{Invertible}(a b) \\text{ with } (a b)^{-1} = b^{-1} a^{-1}$$$

Lean4

/-- A copy of `invertibleMul` for dot notation. -/
abbrev mul [Monoid α] {a b : α} (_ : Invertible a) (_ : Invertible b) : Invertible (a * b) :=
  invertibleMul _ _

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