mul_right_bijective_of_finite₀ — Mathlib

English

In a finite cancellative monoid with zero, right multiplication by a nonzero element is bijective.

Русский

В конечном монойде с нулём, правое умножение на ненулевой элемент биективно.

LaTeX

$$$[CancelMonoidWithZero M] [Finite M] \\; \\Rightarrow \\forall a\\,(ha: a \\neq 0), Bijective(b \\mapsto a*b)$$$

Lean4

theorem mul_right_bijective_of_finite₀ {a : M} (ha : a ≠ 0) : Bijective fun b => a * b :=
  Finite.injective_iff_bijective.1 <| mul_right_injective₀ ha

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