Regular_Representation_wrt_Cancellable_Element_on_Finite_Semigroup_is_Bijection

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cancellabilityproofwikiregular-representationssemigroups

Let $\left({S, \circ}\right)$ be a finite semigroup. Let $a \in S$ be cancellable. Then the left regular representation $\lambda_a$ and the right regular representation $\rho_a$ of $\left({S, \circ}\right)$ with respect to $a$ are both bijections.

Preamble

import Mathlib.Data.Fintype.Card
import Mathlib.Algebra.Group.Defs

Formal statement

theorem Regular_Representation_wrt_Cancellable_Element_on_Finite_Semigroup_is_Bijection {S : Type _} [Fintype S] [Mul S] (a : S) (hL : ∀ b c : S, a * b = a * c → b = c) (hR : ∀ b c : S, b * a = c * a → b = c) : Function.Bijective (λ x => a * x) := by sorry

Source

https://proofwiki.org/wiki/Regular_Representation_wrt_Cancellable_Element_on_Finite_Semigroup_is_Bijection

View graph