scilib documentation

group_theory.perm.basic

The group of permutations (self-equivalences) of a type α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the group structure on equiv.perm α.

source
@[protected, instance]
def equiv.perm.perm_group {α : Type u} :
group (equiv.perm α)
Equations
source
@[simp]
theorem equiv.perm.default_eq {α : Type u} :
inhabited.default = 1
source
@[simp]
theorem equiv.perm.coe_equiv_units_End_apply {α : Type u} (e : equiv.perm α) (ᾰ : α) :
↑(⇑equiv.perm.equiv_units_End e) ᾰ = ⇑e ᾰ
source
@[simp]
theorem equiv.perm.coe_inv_equiv_units_End_apply {α : Type u} (e : equiv.perm α) (ᾰ : α) :
↑(⇑equiv.perm.equiv_units_End e)⁻¹ ᾰ = ⇑(equiv.symm e) ᾰ
source
@[simp]
theorem equiv.perm.equiv_units_End_symm_apply_symm_apply {α : Type u} (u : (function.End α)ˣ) :
⇑(equiv.symm (⇑(equiv.perm.equiv_units_End.symm) u)) = ↑u⁻¹
source
@[simp]
theorem equiv.perm.equiv_units_End_symm_apply_apply {α : Type u} (u : (function.End α)ˣ) :
⇑(⇑(equiv.perm.equiv_units_End.symm) u) = ↑u
source
def equiv.perm.equiv_units_End {α : Type u} :
equiv.perm α ≃* (function.End α)ˣ

The permutation of a type is equivalent to the units group of the endomorphisms monoid of this type.

Equations
source
def monoid_hom.to_hom_perm {α : Type u} {G : Type u_1} [group G] (f : G →* function.End α) :
G →* equiv.perm α

Lift a monoid homomorphism f : G →* function.End α to a monoid homomorphism f : G →* equiv.perm α.

Equations
source
@[simp]
theorem monoid_hom.to_hom_perm_apply_apply {α : Type u} {G : Type u_1} [group G] (f : G →* function.End α) (ᾰ : G) :
⇑(⇑(f.to_hom_perm) ᾰ) = ⇑f ᾰ
source
@[simp]
theorem monoid_hom.to_hom_perm_apply_symm_apply {α : Type u} {G : Type u_1} [group G] (f : G →* function.End α) (ᾰ : G) :
⇑(equiv.symm (⇑(f.to_hom_perm) ᾰ)) = ↑(⇑(f.to_hom_units) ᾰ)⁻¹
source
theorem equiv.perm.mul_apply {α : Type u} (f g : equiv.perm α) (x : α) :
⇑(f * g) x = ⇑f (⇑g x)
source
theorem equiv.perm.one_apply {α : Type u} (x : α) :
⇑1 x = x
source
@[simp]
theorem equiv.perm.inv_apply_self {α : Type u} (f : equiv.perm α) (x : α) :
⇑f⁻¹ (⇑f x) = x
source
@[simp]
theorem equiv.perm.apply_inv_self {α : Type u} (f : equiv.perm α) (x : α) :
⇑f (⇑f⁻¹ x) = x
source
theorem equiv.perm.one_def {α : Type u} :
1 = equiv.refl α
source
theorem equiv.perm.mul_def {α : Type u} (f g : equiv.perm α) :
f * g = equiv.trans g f
source
theorem equiv.perm.inv_def {α : Type u} (f : equiv.perm α) :
f⁻¹ = equiv.symm f
source
@[simp, norm_cast]
theorem equiv.perm.coe_one {α : Type u} :
⇑1 = id
source
@[simp, norm_cast]
theorem equiv.perm.coe_mul {α : Type u} (f g : equiv.perm α) :
⇑(f * g) = ⇑f ∘ ⇑g
source
@[norm_cast]
theorem equiv.perm.coe_pow {α : Type u} (f : equiv.perm α) (n : ℕ) :
⇑(f ^ n) = (⇑f^[n])
source
@[simp]
theorem equiv.perm.iterate_eq_pow {α : Type u} (f : equiv.perm α) (n : ℕ) :
⇑f^[n] = ⇑(f ^ n)
source
theorem equiv.perm.eq_inv_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :
x = ⇑f⁻¹ y ↔ ⇑f x = y
source
theorem equiv.perm.inv_eq_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :
⇑f⁻¹ x = y ↔ x = ⇑f y
source
theorem equiv.perm.zpow_apply_comm {α : Type u_1} (σ : equiv.perm α) (m n : ℤ) {x : α} :
⇑(σ ^ m) (⇑(σ ^ n) x) = ⇑(σ ^ n) (⇑(σ ^ m) x)
source
@[simp]
theorem equiv.perm.image_inv {α : Type u} (f : equiv.perm α) (s : set α) :
⇑f⁻¹ '' s = ⇑f ⁻¹' s
source
@[simp]
theorem equiv.perm.preimage_inv {α : Type u} (f : equiv.perm α) (s : set α) :
⇑f⁻¹ ⁻¹' s = ⇑f '' s

Lemmas about mixing perm with equiv. Because we have multiple ways to express equiv.refl, equiv.symm, and equiv.trans, we want simp lemmas for every combination. The assumption made here is that if you're using the group structure, you want to preserve it after simp.

source
@[simp]
theorem equiv.perm.trans_one {α : Sort u_1} {β : Type u_2} (e : α ≃ β) :
e.trans 1 = e
source
@[simp]
theorem equiv.perm.mul_refl {α : Type u} (e : equiv.perm α) :
e * equiv.refl α = e
source
@[simp]
theorem equiv.perm.one_symm {α : Type u} :
equiv.symm 1 = 1
source
@[simp]
theorem equiv.perm.refl_inv {α : Type u} :
(equiv.refl α)⁻¹ = 1
source
@[simp]
theorem equiv.perm.one_trans {α : Type u_1} {β : Sort u_2} (e : α ≃ β) :
equiv.trans 1 e = e
source
@[simp]
theorem equiv.perm.refl_mul {α : Type u} (e : equiv.perm α) :
equiv.refl α * e = e
source
@[simp]
theorem equiv.perm.inv_trans_self {α : Type u} (e : equiv.perm α) :
equiv.trans e⁻¹ e = 1
source
@[simp]
theorem equiv.perm.mul_symm {α : Type u} (e : equiv.perm α) :
e * equiv.symm e = 1
source
@[simp]
theorem equiv.perm.self_trans_inv {α : Type u} (e : equiv.perm α) :
equiv.trans e e⁻¹ = 1
source
@[simp]
theorem equiv.perm.symm_mul {α : Type u} (e : equiv.perm α) :
equiv.symm e * e = 1

Lemmas about equiv.perm.sum_congr re-expressed via the group structure.

source
@[simp]
theorem equiv.perm.sum_congr_mul {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) (g : equiv.perm α) (h : equiv.perm β) :
e.sum_congr f * g.sum_congr h = (e * g).sum_congr (f * h)
source
@[simp]
theorem equiv.perm.sum_congr_inv {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) :
(e.sum_congr f)⁻¹ = e⁻¹.sum_congr f⁻¹
source
@[simp]
theorem equiv.perm.sum_congr_one {α : Type u_1} {β : Type u_2} :
1.sum_congr 1 = 1
source
@[simp]
theorem equiv.perm.sum_congr_hom_apply (α : Type u_1) (β : Type u_2) (a : equiv.perm α × equiv.perm β) :
⇑(equiv.perm.sum_congr_hom α β) a = a.fst.sum_congr a.snd
source
def equiv.perm.sum_congr_hom (α : Type u_1) (β : Type u_2) :
equiv.perm α × equiv.perm β →* equiv.perm (α ⊕ β)

equiv.perm.sum_congr as a monoid_hom, with its two arguments bundled into a single prod.

This is particularly useful for its monoid_hom.range projection, which is the subgroup of permutations which do not exchange elements between α and β.

Equations
source
theorem equiv.perm.sum_congr_hom_injective {α : Type u_1} {β : Type u_2} :
function.injective ⇑(equiv.perm.sum_congr_hom α β)
source
@[simp]
theorem equiv.perm.sum_congr_swap_one {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : α) :
(equiv.swap i j).sum_congr 1 = equiv.swap (sum.inl i) (sum.inl j)
source
@[simp]
theorem equiv.perm.sum_congr_one_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : β) :
1.sum_congr (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j)

Lemmas about equiv.perm.sigma_congr_right re-expressed via the group structure.

source
@[simp]
theorem equiv.perm.sigma_congr_right_mul {α : Type u_1} {β : α → Type u_2} (F G : Π (a : α), equiv.perm (β a)) :
equiv.perm.sigma_congr_right F * equiv.perm.sigma_congr_right G = equiv.perm.sigma_congr_right (F * G)
source
@[simp]
theorem equiv.perm.sigma_congr_right_inv {α : Type u_1} {β : α → Type u_2} (F : Π (a : α), equiv.perm (β a)) :
(equiv.perm.sigma_congr_right F)⁻¹ = equiv.perm.sigma_congr_right (λ (a : α), (F a)⁻¹)
source
@[simp]
theorem equiv.perm.sigma_congr_right_one {α : Type u_1} {β : α → Type u_2} :
equiv.perm.sigma_congr_right 1 = 1
source
@[simp]
theorem equiv.perm.sigma_congr_right_hom_apply {α : Type u_1} (β : α → Type u_2) (F : Π (a : α), equiv.perm ((λ (a : α), β a) a)) :
⇑(equiv.perm.sigma_congr_right_hom β) F = equiv.perm.sigma_congr_right F
source
def equiv.perm.sigma_congr_right_hom {α : Type u_1} (β : α → Type u_2) :
(Π (a : α), equiv.perm (β a)) →* equiv.perm (Σ (a : α), β a)

equiv.perm.sigma_congr_right as a monoid_hom.

This is particularly useful for its monoid_hom.range projection, which is the subgroup of permutations which do not exchange elements between fibers.

Equations
source
theorem equiv.perm.sigma_congr_right_hom_injective {α : Type u_1} {β : α → Type u_2} :
function.injective ⇑(equiv.perm.sigma_congr_right_hom β)
source
@[simp]
theorem equiv.perm.subtype_congr_hom_apply {α : Type u} (p : α → Prop) [decidable_pred p] (pair : equiv.perm {a // p a} × equiv.perm {a // ¬p a}) :
⇑(equiv.perm.subtype_congr_hom p) pair = pair.fst.subtype_congr pair.snd
source
def equiv.perm.subtype_congr_hom {α : Type u} (p : α → Prop) [decidable_pred p] :
equiv.perm {a // p a} × equiv.perm {a // ¬p a} →* equiv.perm α

equiv.perm.subtype_congr as a monoid_hom.

Equations
source
theorem equiv.perm.subtype_congr_hom_injective {α : Type u} (p : α → Prop) [decidable_pred p] :
function.injective ⇑(equiv.perm.subtype_congr_hom p)
source
@[simp]
theorem equiv.perm.perm_congr_eq_mul {α : Type u} (e p : equiv.perm α) :
⇑(equiv.perm_congr e) p = e * p * e⁻¹

If e is also a permutation, we can write perm_congr completely in terms of the group structure.

Lemmas about equiv.perm.extend_domain re-expressed via the group structure.

source
@[simp]
theorem equiv.perm.extend_domain_one {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) :
1.extend_domain f = 1
source
@[simp]
theorem equiv.perm.extend_domain_inv {α : Type u} {β : Type v} (e : equiv.perm α) {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) :
(e.extend_domain f)⁻¹ = e⁻¹.extend_domain f
source
@[simp]
theorem equiv.perm.extend_domain_mul {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) (e e' : equiv.perm α) :
e.extend_domain f * e'.extend_domain f = (e * e').extend_domain f
source
@[simp]
theorem equiv.perm.extend_domain_hom_apply {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) (e : equiv.perm α) :
⇑(equiv.perm.extend_domain_hom f) e = e.extend_domain f
source
def equiv.perm.extend_domain_hom {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) :
equiv.perm α →* equiv.perm β

extend_domain as a group homomorphism

Equations
source
theorem equiv.perm.extend_domain_hom_injective {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) :
function.injective ⇑(equiv.perm.extend_domain_hom f)
source
@[simp]
theorem equiv.perm.extend_domain_eq_one_iff {α : Type u} {β : Type v} {p : β → Prop} [decidable_pred p] {e : equiv.perm α} {f : α ≃ subtype p} :
e.extend_domain f = 1 ↔ e = 1
source
@[simp]
theorem equiv.perm.extend_domain_pow {α : Type u} {β : Type v} (e : equiv.perm α) {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) (n : ℕ) :
(e ^ n).extend_domain f = e.extend_domain f ^ n
source
@[simp]
theorem equiv.perm.extend_domain_zpow {α : Type u} {β : Type v} (e : equiv.perm α) {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) (n : ℤ) :
(e ^ n).extend_domain f = e.extend_domain f ^ n
source
def equiv.perm.subtype_perm {α : Type u} {p : α → Prop} (f : equiv.perm α) (h : ∀ (x : α), p x ↔ p (⇑f x)) :
equiv.perm {x // p x}

If the permutation f fixes the subtype {x // p x}, then this returns the permutation on {x // p x} induced by f.

Equations
source
@[simp]
theorem equiv.perm.subtype_perm_apply {α : Type u} {p : α → Prop} (f : equiv.perm α) (h : ∀ (x : α), p x ↔ p (⇑f x)) (x : {x // p x}) :
⇑(f.subtype_perm h) x = ⟨⇑f ↑x, _⟩
source
@[simp]
theorem equiv.perm.subtype_perm_one {α : Type u} (p : α → Prop) (h : (∀ (_x : α), p _x ↔ p _x) := _) :
1.subtype_perm h = 1
source
@[simp]
theorem equiv.perm.subtype_perm_mul {α : Type u} {p : α → Prop} (f g : equiv.perm α) (hf : ∀ (x : α), p x ↔ p (⇑f x)) (hg : ∀ (x : α), p x ↔ p (⇑g x)) :
f.subtype_perm hf * g.subtype_perm hg = (f * g).subtype_perm _
source
theorem equiv.perm.subtype_perm_inv {α : Type u} {p : α → Prop} (f : equiv.perm α) (hf : ∀ (x : α), p x ↔ p (⇑f⁻¹ x)) :
f⁻¹.subtype_perm hf = (f.subtype_perm _)⁻¹

See equiv.perm.inv_subtype_perm

source
@[simp]
theorem equiv.perm.inv_subtype_perm {α : Type u} {p : α → Prop} (f : equiv.perm α) (hf : ∀ (x : α), p x ↔ p (⇑f x)) :
(f.subtype_perm hf)⁻¹ = f⁻¹.subtype_perm _

See equiv.perm.subtype_perm_inv

source
@[simp]
theorem equiv.perm.subtype_perm_pow {α : Type u} {p : α → Prop} (f : equiv.perm α) (n : ℕ) (hf : ∀ (x : α), p x ↔ p (⇑f x)) :
f.subtype_perm hf ^ n = (f ^ n).subtype_perm _
source
@[simp]
theorem equiv.perm.subtype_perm_zpow {α : Type u} {p : α → Prop} (f : equiv.perm α) (n : ℤ) (hf : ∀ (x : α), p x ↔ p (⇑f x)) :
f.subtype_perm hf ^ n = (f ^ n).subtype_perm _
source
def equiv.perm.of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] :
equiv.perm (subtype p) →* equiv.perm α

The inclusion map of permutations on a subtype of α into permutations of α, fixing the other points.

Equations
source
theorem equiv.perm.of_subtype_subtype_perm {α : Type u} {p : α → Prop} [decidable_pred p] {f : equiv.perm α} (h₁ : ∀ (x : α), p x ↔ p (⇑f x)) (h₂ : ∀ (x : α), ⇑f x ≠ x → p x) :
⇑equiv.perm.of_subtype (f.subtype_perm h₁) = f
source
theorem equiv.perm.of_subtype_apply_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (f : equiv.perm (subtype p)) (ha : p a) :
⇑(⇑equiv.perm.of_subtype f) a = ↑(⇑f ⟨a, ha⟩)
source
@[simp]
theorem equiv.perm.of_subtype_apply_coe {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) (x : subtype p) :
⇑(⇑equiv.perm.of_subtype f) ↑x = ↑(⇑f x)
source
theorem equiv.perm.of_subtype_apply_of_not_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (f : equiv.perm (subtype p)) (ha : ¬p a) :
⇑(⇑equiv.perm.of_subtype f) a = a
source
theorem equiv.perm.mem_iff_of_subtype_apply_mem {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) (x : α) :
p x ↔ p (⇑(⇑equiv.perm.of_subtype f) x)
source
@[simp]
theorem equiv.perm.subtype_perm_of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) :
(⇑equiv.perm.of_subtype f).subtype_perm _ = f
source
@[simp]
theorem equiv.perm.subtype_equiv_subtype_perm_apply_coe {α : Type u} (p : α → Prop) [decidable_pred p] (f : equiv.perm (subtype p)) :
↑(⇑(equiv.perm.subtype_equiv_subtype_perm p) f) = ⇑equiv.perm.of_subtype f
source
@[simp]
theorem equiv.perm.subtype_equiv_subtype_perm_symm_apply {α : Type u} (p : α → Prop) [decidable_pred p] (f : {f // ∀ (a : α), ¬p a → ⇑f a = a}) :
⇑((equiv.perm.subtype_equiv_subtype_perm p).symm) f = ↑f.subtype_perm _
source
@[protected]
def equiv.perm.subtype_equiv_subtype_perm {α : Type u} (p : α → Prop) [decidable_pred p] :
equiv.perm (subtype p) ≃ {f // ∀ (a : α), ¬p a → ⇑f a = a}

Permutations on a subtype are equivalent to permutations on the original type that fix pointwise the rest.

Equations
source
theorem equiv.perm.subtype_equiv_subtype_perm_apply_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (f : equiv.perm (subtype p)) (h : p a) :
⇑(⇑(equiv.perm.subtype_equiv_subtype_perm p) f) a = ↑(⇑f ⟨a, h⟩)
source
theorem equiv.perm.subtype_equiv_subtype_perm_apply_of_not_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (f : equiv.perm (subtype p)) (h : ¬p a) :
⇑(⇑(equiv.perm.subtype_equiv_subtype_perm p) f) a = a
source
@[simp]
theorem equiv.swap_inv {α : Type u} [decidable_eq α] (x y : α) :
(equiv.swap x y)⁻¹ = equiv.swap x y
source
@[simp]
theorem equiv.swap_mul_self {α : Type u} [decidable_eq α] (i j : α) :
equiv.swap i j * equiv.swap i j = 1
source
theorem equiv.swap_mul_eq_mul_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :
equiv.swap x y * f = f * equiv.swap (⇑f⁻¹ x) (⇑f⁻¹ y)
source
theorem equiv.mul_swap_eq_swap_mul {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :
f * equiv.swap x y = equiv.swap (⇑f x) (⇑f y) * f
source
theorem equiv.swap_apply_apply {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :
equiv.swap (⇑f x) (⇑f y) = f * equiv.swap x y * f⁻¹
source
@[simp]
theorem equiv.swap_mul_self_mul {α : Type u} [decidable_eq α] (i j : α) (σ : equiv.perm α) :
equiv.swap i j * (equiv.swap i j * σ) = σ

Left-multiplying a permutation with swap i j twice gives the original permutation.

This specialization of swap_mul_self is useful when using cosets of permutations.

source
@[simp]
theorem equiv.mul_swap_mul_self {α : Type u} [decidable_eq α] (i j : α) (σ : equiv.perm α) :
σ * equiv.swap i j * equiv.swap i j = σ

Right-multiplying a permutation with swap i j twice gives the original permutation.

This specialization of swap_mul_self is useful when using cosets of permutations.

source
@[simp]
theorem equiv.swap_mul_involutive {α : Type u} [decidable_eq α] (i j : α) :
function.involutive (has_mul.mul (equiv.swap i j))

A stronger version of mul_right_injective

source
@[simp]
theorem equiv.mul_swap_involutive {α : Type u} [decidable_eq α] (i j : α) :
function.involutive (λ (_x : equiv.perm α), _x * equiv.swap i j)

A stronger version of mul_left_injective

source
@[simp]
theorem equiv.swap_eq_one_iff {α : Type u} [decidable_eq α] {i j : α} :
equiv.swap i j = 1 ↔ i = j
source
theorem equiv.swap_mul_eq_iff {α : Type u} [decidable_eq α] {i j : α} {σ : equiv.perm α} :
equiv.swap i j * σ = σ ↔ i = j
source
theorem equiv.mul_swap_eq_iff {α : Type u} [decidable_eq α] {i j : α} {σ : equiv.perm α} :
σ * equiv.swap i j = σ ↔ i = j
source
theorem equiv.swap_mul_swap_mul_swap {α : Type u} [decidable_eq α] {x y z : α} (hwz : x ≠ y) (hxz : x ≠ z) :
equiv.swap y z * equiv.swap x y * equiv.swap y z = equiv.swap z x
source
@[simp]
theorem equiv.add_left_zero {α : Type u} [add_group α] :
equiv.add_left 0 = 1
source
@[simp]
theorem equiv.add_right_zero {α : Type u} [add_group α] :
equiv.add_right 0 = 1
source
@[simp]
theorem equiv.add_left_add {α : Type u} [add_group α] (a b : α) :
equiv.add_left (a + b) = equiv.add_left a * equiv.add_left b
source
@[simp]
theorem equiv.add_right_add {α : Type u} [add_group α] (a b : α) :
equiv.add_right (a + b) = equiv.add_right b * equiv.add_right a
source
@[simp]
theorem equiv.inv_add_left {α : Type u} [add_group α] (a : α) :
(equiv.add_left a)⁻¹ = equiv.add_left (-a)
source
@[simp]
theorem equiv.inv_add_right {α : Type u} [add_group α] (a : α) :
(equiv.add_right a)⁻¹ = equiv.add_right (-a)
source
@[simp]
theorem equiv.pow_add_left {α : Type u} [add_group α] (a : α) (n : ℕ) :
equiv.add_left a ^ n = equiv.add_left (n • a)
source
@[simp]
theorem equiv.pow_add_right {α : Type u} [add_group α] (a : α) (n : ℕ) :
equiv.add_right a ^ n = equiv.add_right (n • a)
source
@[simp]
theorem equiv.zpow_add_left {α : Type u} [add_group α] (a : α) (n : ℤ) :
equiv.add_left a ^ n = equiv.add_left (n • a)
source
@[simp]
theorem equiv.zpow_add_right {α : Type u} [add_group α] (a : α) (n : ℤ) :
equiv.add_right a ^ n = equiv.add_right (n • a)
source
@[simp]
theorem equiv.mul_left_one {α : Type u} [group α] :
equiv.mul_left 1 = 1
source
@[simp]
theorem equiv.mul_right_one {α : Type u} [group α] :
equiv.mul_right 1 = 1
source
@[simp]
theorem equiv.mul_left_mul {α : Type u} [group α] (a b : α) :
equiv.mul_left (a * b) = equiv.mul_left a * equiv.mul_left b
source
@[simp]
theorem equiv.mul_right_mul {α : Type u} [group α] (a b : α) :
equiv.mul_right (a * b) = equiv.mul_right b * equiv.mul_right a
source
@[simp]
theorem equiv.inv_mul_left {α : Type u} [group α] (a : α) :
(equiv.mul_left a)⁻¹ = equiv.mul_left a⁻¹
source
@[simp]
theorem equiv.inv_mul_right {α : Type u} [group α] (a : α) :
(equiv.mul_right a)⁻¹ = equiv.mul_right a⁻¹
source
@[simp]
theorem equiv.pow_mul_left {α : Type u} [group α] (a : α) (n : ℕ) :
equiv.mul_left a ^ n = equiv.mul_left (a ^ n)
source
@[simp]
theorem equiv.pow_mul_right {α : Type u} [group α] (a : α) (n : ℕ) :
equiv.mul_right a ^ n = equiv.mul_right (a ^ n)
source
@[simp]
theorem equiv.zpow_mul_left {α : Type u} [group α] (a : α) (n : ℤ) :
equiv.mul_left a ^ n = equiv.mul_left (a ^ n)
source
@[simp]
theorem equiv.zpow_mul_right {α : Type u} [group α] (a : α) (n : ℤ) :
equiv.mul_right a ^ n = equiv.mul_right (a ^ n)
source
@[simp]
theorem set.bij_on_perm_inv {α : Type u_1} {f : equiv.perm α} {s t : set α} :
set.bij_on ⇑f⁻¹ t s ↔ set.bij_on ⇑f s t
source
theorem set.bij_on.of_perm_inv {α : Type u_1} {f : equiv.perm α} {s t : set α} :
set.bij_on ⇑f⁻¹ t s → set.bij_on ⇑f s t

Alias of the forward direction of set.bij_on_perm_inv.

source
theorem set.bij_on.perm_inv {α : Type u_1} {f : equiv.perm α} {s t : set α} :
set.bij_on ⇑f s t → set.bij_on ⇑f⁻¹ t s

Alias of the reverse direction of set.bij_on_perm_inv.

source
theorem set.maps_to.perm_pow {α : Type u_1} {f : equiv.perm α} {s : set α} :
set.maps_to ⇑f s s → ∀ (n : ℕ), set.maps_to ⇑(f ^ n) s s
source
theorem set.surj_on.perm_pow {α : Type u_1} {f : equiv.perm α} {s : set α} :
set.surj_on ⇑f s s → ∀ (n : ℕ), set.surj_on ⇑(f ^ n) s s
source
theorem set.bij_on.perm_pow {α : Type u_1} {f : equiv.perm α} {s : set α} :
set.bij_on ⇑f s s → ∀ (n : ℕ), set.bij_on ⇑(f ^ n) s s
source
theorem set.bij_on.perm_zpow {α : Type u_1} {f : equiv.perm α} {s : set α} (hf : set.bij_on ⇑f s s) (n : ℤ) :
set.bij_on ⇑(f ^ n) s s