smul_bijective — Mathlib

English

If m is a unit in α, then the map a ↦ m • a is bijective.

Русский

Если m — единица в моноиде α, отображение a ↦ m • a биективно.

LaTeX

$$$ \text{smul_bijective} \{m : \alpha\} (hm : \text{IsUnit } m) : \text{Bijective } (\lambda a, m \cdot a)$$$

Lean4

@[to_additive]
theorem smul_bijective {m : α} (hm : IsUnit m) : Function.Bijective (fun (a : β) ↦ m • a) :=
  by
  lift m to αˣ using hm
  exact MulAction.bijective m

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