/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.2
G : 
Type _: Type (?u.2+1)
Type _}

namespace Equiv

section GroupWithZero

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

/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type. -/
@[simps! (config := { fullyApplied := 
false: Bool
false })]
protected def 
mulLeft₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm G
mulLeft₀ (
a: G
a : 
G: Type ?u.11
G) (
ha: a ≠ 0
ha : 
a: G
a ≠ 
0: ?m.22
0) : 
Perm: Sort ?u.76 → Sort (max1?u.76)
Perm 
G: Type ?u.11
G :=
  (
Units.mk0: {G₀ : Type ?u.82} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣ
Units.mk0 
a: G
a 
ha: a ≠ 0
ha).
mulLeft: {M : Type ?u.96} → [inst : Monoid M] → Mˣ → Perm M
mulLeft
#align equiv.mul_left₀ 
Equiv.mulLeft₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm G
Equiv.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⁻¹ * x
Equiv.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 * x
Equiv.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: G
a : 
G: Type ?u.843
G) (
ha: a ≠ 0
ha : 
a: G
a ≠ 
0: ?m.854
0) : 
Function.Bijective: {α : Sort ?u.909} → {β : Sort ?u.908} → (α → β) → Prop
Function.Bijective (
(· * ·): G → G → G
(· * ·) 
a: G
a : 
G: Type ?u.843
G → 
G: Type ?u.843
G) :=
  (
Equiv.mulLeft₀: {G : Type ?u.1005} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm G
Equiv.mulLeft₀ 
a: G
a 
ha: a ≠ 0
ha).
bijective: ∀ {α : Sort ?u.1022} {β : Sort ?u.1021} (e : α ≃ β), Function.Bijective ↑e
bijective
#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: Bool
false })]
protected def 
mulRight₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm G
mulRight₀ (
a: G
a : 
G: Type ?u.1046
G) (
ha: a ≠ 0
ha : 
a: G
a ≠ 
0: ?m.1057
0) : 
Perm: Sort ?u.1111 → Sort (max1?u.1111)
Perm 
G: Type ?u.1046
G :=
  (
Units.mk0: {G₀ : Type ?u.1117} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣ
Units.mk0 
a: G
a 
ha: a ≠ 0
ha).
mulRight: {M : Type ?u.1131} → [inst : Monoid M] → Mˣ → Perm M
mulRight
#align equiv.mul_right₀ 
Equiv.mulRight₀: {G : Type u_1} → [inst : GroupWithZero G] → (a : G) → a ≠ 0 → Perm G
Equiv.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 * a
Equiv.mulRight₀_apply

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

end GroupWithZero

end Equiv