mul_left_bijective_of_finite₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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