mulRight_bijective₀

Mathlib.Algebra.GroupWithZero.Units.Equiv

URI: https://scilib.ai/kg/mathlib#mulRight_bijective₀

English

If a ≠ 0, then the map x ↦ x a is bijective on G₀.

Русский

Если a ≠ 0, то отображение x ↦ x a биективно на G₀.

LaTeX

$$$a \\neq 0 \\Rightarrow \\text{Bijective}(x \\mapsto x a)$$$

Lean4

theorem _root_.mulRight_bijective₀ (a : G₀) (ha : a ≠ 0) : Function.Bijective ((· * a) : G₀ → G₀) :=
  (Equiv.mulRight₀ a ha).bijective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru