Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.hom.equiv.units.group_with_zero
! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Equiv.Units.Basic
import Mathlib.Algebra.GroupWithZero.Units.Basic

/-!
# Multiplication by a nonzero element in a `GroupWithZero` is a permutation.
-/

variable {G: Type ?u.2G : Type _: Type (?u.2+1)Type _}

namespace Equiv

section GroupWithZero

variable [GroupWithZero: Type ?u.1049 → Type ?u.1049GroupWithZero G: Type ?u.5G]

/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! (config := { fullyApplied := false: Boolfalse })]
protected def mulLeft₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GmulLeft₀ (a: Ga : G: Type ?u.11G) (ha: a ≠ 0ha : a: Ga ≠ 0: ?m.220) : Perm: Sort ?u.76 → Sort (max1?u.76)Perm G: Type ?u.11G :=
(Units.mk0: {G₀ : Type ?u.82} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣUnits.mk0 a: Ga ha: a ≠ 0ha).mulLeft: {M : Type ?u.96} → [inst : Monoid M] → Mˣ → Perm MmulLeft
#align equiv.mul_left₀ Equiv.mulLeft₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GEquiv.mulLeft₀
#align equiv.mul_left₀_symm_apply Equiv.mulLeft₀_symm_apply: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G) (ha : a ≠ 0), ↑(Equiv.mulLeft₀ a ha).symm = fun x => a⁻¹ * xEquiv.mulLeft₀_symm_apply
#align equiv.mul_left₀_apply Equiv.mulLeft₀_apply: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G) (ha : a ≠ 0), ↑(Equiv.mulLeft₀ a ha) = fun x => a * xEquiv.mulLeft₀_apply

theorem _root_.mulLeft_bijective₀: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G), a ≠ 0 → Function.Bijective ((fun x x_1 => x * x_1) a)_root_.mulLeft_bijective₀ (a: Ga : G: Type ?u.843G) (ha: a ≠ 0ha : a: Ga ≠ 0: ?m.8540) : Function.Bijective: {α : Sort ?u.909} → {β : Sort ?u.908} → (α → β) → PropFunction.Bijective ((· * ·): G → G → G(· * ·) a: Ga : G: Type ?u.843G → G: Type ?u.843G) :=
(Equiv.mulLeft₀: {G : Type ?u.1005} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GEquiv.mulLeft₀ a: Ga ha: a ≠ 0ha).bijective: ∀ {α : Sort ?u.1022} {β : Sort ?u.1021} (e : α ≃ β), Function.Bijective ↑ebijective
#align mul_left_bijective₀ mulLeft_bijective₀: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G), a ≠ 0 → Function.Bijective ((fun x x_1 => x * x_1) a)mulLeft_bijective₀

/-- Right multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! (config := { fullyApplied := false: Boolfalse })]
protected def mulRight₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GmulRight₀ (a: Ga : G: Type ?u.1046G) (ha: a ≠ 0ha : a: Ga ≠ 0: ?m.10570) : Perm: Sort ?u.1111 → Sort (max1?u.1111)Perm G: Type ?u.1046G :=
(Units.mk0: {G₀ : Type ?u.1117} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣUnits.mk0 a: Ga ha: a ≠ 0ha).mulRight: {M : Type ?u.1131} → [inst : Monoid M] → Mˣ → Perm MmulRight
#align equiv.mul_right₀ Equiv.mulRight₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GEquiv.mulRight₀
#align equiv.mul_right₀_symm_apply Equiv.mulRight₀_symm_apply: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G) (ha : a ≠ 0), ↑(Equiv.mulRight₀ a ha).symm = fun x => x * a⁻¹Equiv.mulRight₀_symm_apply
#align equiv.mul_right₀_apply Equiv.mulRight₀_apply: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G) (ha : a ≠ 0), ↑(Equiv.mulRight₀ a ha) = fun x => x * aEquiv.mulRight₀_apply

theorem _root_.mulRight_bijective₀: ∀ (a : G), a ≠ 0 → Function.Bijective fun x => x * a_root_.mulRight_bijective₀ (a: Ga : G: Type ?u.2165G) (ha: a ≠ 0ha : a: Ga ≠ 0: ?m.21760) : Function.Bijective: {α : Sort ?u.2231} → {β : Sort ?u.2230} → (α → β) → PropFunction.Bijective ((· * a: Ga) : G: Type ?u.2165G → G: Type ?u.2165G) :=
(Equiv.mulRight₀: {G : Type ?u.2322} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm GEquiv.mulRight₀ a: Ga ha: a ≠ 0ha).bijective: ∀ {α : Sort ?u.2339} {β : Sort ?u.2338} (e : α ≃ β), Function.Bijective ↑ebijective
#align mul_right_bijective₀ mulRight_bijective₀: ∀ {G : Type u_1} [inst : GroupWithZero G] (a : G), a ≠ 0 → Function.Bijective fun x => x * amulRight_bijective₀

end GroupWithZero

end Equiv
```