Mathlib.Algebra.GroupWithZero.Units.Equiv

unitsEquivNeZero definition

: G₀ˣ ≃ { a : G₀ // a ≠ 0 }

Full source

/-- In a `GroupWithZero` `G₀`, the unit group `G₀ˣ` is equivalent to the subtype of nonzero
elements. -/
@[simps] def _root_.unitsEquivNeZero : G₀ˣG₀ˣ ≃ {a : G₀ // a ≠ 0} where
  toFun a := ⟨a, a.ne_zero⟩
  invFun a := Units.mk0 _ a.prop
  left_inv _ := Units.ext rfl
  right_inv _ := rfl

Equivalence between units and nonzero elements in a group with zero

Informal description

In a group with zero $ G_0 $, the group of units $ G_0^\times $ is equivalent to the subtype of nonzero elements $ \{a \in G_0 \mid a \neq 0\} $. The equivalence is given by: - The forward map sends a unit $ a \in G_0^\times $ to its underlying element $ a \in G_0 $ (which is nonzero by definition). - The inverse map constructs a unit from a nonzero element $ a \in G_0 $ using its multiplicative inverse $ a^{-1} $. This equivalence is a bijection, with the left inverse being the identity on $ G_0^\times $ and the right inverse being the identity on the subtype of nonzero elements.

Equiv.mulLeft₀ definition

(a : G₀) (ha : a ≠ 0) : Perm G₀

Full source

/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! -fullyApplied]
protected def mulLeft₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ :=
  (Units.mk0 a ha).mulLeft

Left multiplication by a nonzero element as a permutation

Informal description

For any nonzero element $ a $ in a group with zero $ G_0 $, the left multiplication map $ x \mapsto a \cdot x $ is a permutation of $ G_0 $. The inverse of this permutation is given by left multiplication by $ a^{-1} $.

mulLeft_bijective₀ theorem

(a : G₀) (ha : a ≠ 0) : Function.Bijective (a * · : G₀ → G₀)

Full source

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

Bijectivity of Left Multiplication by a Nonzero Element in a Group with Zero

Informal description

For any nonzero element $a$ in a group with zero $G_0$, the left multiplication map $x \mapsto a \cdot x$ is bijective on $G_0$.

Equiv.mulRight₀ definition

(a : G₀) (ha : a ≠ 0) : Perm G₀

Full source

/-- Right multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! -fullyApplied]
protected def mulRight₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ :=
  (Units.mk0 a ha).mulRight

Permutation induced by right multiplication by a nonzero element in a group with zero

Informal description

For any nonzero element $ a $ in a group with zero $ G_0 $, the function $ x \mapsto x \cdot a $ is a permutation of $ G_0 $. This means it is a bijective map from $ G_0 $ to itself, with the inverse function given by $ x \mapsto x \cdot a^{-1} $.

mulRight_bijective₀ theorem

(a : G₀) (ha : a ≠ 0) : Function.Bijective ((· * a) : G₀ → G₀)

Full source

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

Bijectivity of Right Multiplication by Nonzero Element in Group with Zero

Informal description

For any nonzero element $a$ in a group with zero $G_0$, the right multiplication map $x \mapsto x \cdot a$ is bijective on $G_0$.

Equiv.divRight₀ definition

(a : G₀) (ha : a ≠ 0) : Perm G₀

Full source

/-- Right division by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! +simpRhs]
def divRight₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ where
  toFun := (· / a)
  invFun := (· * a)
  left_inv _ := by simp [ha]
  right_inv _ := by simp [ha]

Permutation induced by right division by a nonzero element in a group with zero

Informal description

For any nonzero element $ a $ in a group with zero $ G_0 $, the function $ x \mapsto x / a $ is a permutation of $ G_0 $. This means it is a bijective map from $ G_0 $ to itself, with the inverse function given by $ x \mapsto x \cdot a $.

Equiv.divLeft₀ definition

(a : G₀) (ha : a ≠ 0) : Perm G₀

Full source

/-- Left division by a nonzero element in a `CommGroupWithZero` is a permutation of the underlying
type. -/
@[simps! +simpRhs]
def divLeft₀ (a : G₀) (ha : a ≠ 0) : Perm G₀ where
  toFun := (a / ·)
  invFun := (a / ·)
  left_inv _ := by simp [ha]
  right_inv _ := by simp [ha]

Permutation induced by left division by a nonzero element in a commutative group with zero

Informal description

For any nonzero element $ a $ in a commutative group with zero $ G_0 $, the function $ x \mapsto a / x $ is a permutation of $ G_0 $. This means it is a bijective map from $ G_0 $ to itself, with the inverse function also given by $ x \mapsto a / x $.