mulLeft_bijective₀

Mathlib.Algebra.GroupWithZero.Units.Equiv

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

English

If a ≠ 0, then the map x ↦ a x is a bijection of G₀.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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