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.
/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

Some proofs and docs came from `algebra/commute` (c) Neil Strickland

! This file was ported from Lean 3 source module algebra.group.semiconj
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Units

/-!
# Semiconjugate elements of a semigroup

## Main definitions

We say that `x` is semiconjugate to `y` by `a` (`SemiconjBy a x y`), if `a * x = y * a`.
In this file we provide operations on `SemiconjBy _ _ _`.

In the names of these operations, we treat `a` as the “left” argument, and both `x` and `y` as
“right” arguments. This way most names in this file agree with the names of the corresponding lemmas
for `Commute a b = SemiconjBy a b b`. As a side effect, some lemmas have only `_right` version.

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like
`rw [(h.pow_right 5).eq]` rather than just `rw [h.pow_right 5]`.

This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` etc). Other
operations (`pow_right`, field inverse etc) are in the files that define corresponding notions.
-/

/-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
@[to_additive 
AddSemiconjBy: {M : Type u_1} → [inst : Add M] → M → M → M → Prop
AddSemiconjBy
"`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"] def
SemiconjBy: {M : Type u_1} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
[
Mul: Type ?u.7 → Type ?u.7
Mul
M: ?m.4
M
] (
a: M
a
x: M
x
y: M
y
:
M: ?m.4
M
) :
Prop: Type
Prop
:=
a: M
a
*
x: M
x
=
y: M
y
*
a: M
a
#align semiconj_by
SemiconjBy: {M : Type u_1} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
#align add_semiconj_by
AddSemiconjBy: {M : Type u_1} → [inst : Add M] → M → M → M → Prop
AddSemiconjBy
namespace SemiconjBy /-- Equality behind `SemiconjBy a x y`; useful for rewriting. -/ @[
to_additive: ∀ {S : Type u_1} [inst : Add S] {a x y : S}, AddSemiconjBy a x y → a + x = y + a
to_additive
"Equality behind `AddSemiconjBy a x y`; useful for rewriting."] protected theorem
eq: ∀ {S : Type u_1} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
eq
[
Mul: Type ?u.131 → Type ?u.131
Mul
S: ?m.128
S
] {
a: S
a
x: S
x
y: S
y
:
S: ?m.128
S
} (
h: SemiconjBy a x y
h
:
SemiconjBy: {M : Type ?u.140} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: S
a
x: S
x
y: S
y
) :
a: S
a
*
x: S
x
=
y: S
y
*
a: S
a
:=
h: SemiconjBy a x y
h
#align semiconj_by.eq
SemiconjBy.eq: ∀ {S : Type u_1} [inst : Mul S] {a x y : S}, SemiconjBy a x y → a * x = y * a
SemiconjBy.eq
#align add_semiconj_by.eq
AddSemiconjBy.eq: ∀ {S : Type u_1} [inst : Add S] {a x y : S}, AddSemiconjBy a x y → a + x = y + a
AddSemiconjBy.eq
section Semigroup variable [
Semigroup: Type ?u.1081 → Type ?u.1081
Semigroup
S: ?m.277
S
] {
a: S
a
b: S
b
x: S
x
y: S
y
z: S
z
x': S
x'
y': S
y'
:
S: ?m.255
S
} /-- If `a` semiconjugates `x` to `y` and `x'` to `y'`, then it semiconjugates `x * x'` to `y * y'`. -/ @[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {a x y x' y' : S}, AddSemiconjBy a x y → AddSemiconjBy a x' y' → AddSemiconjBy a (x + x') (y + y')
to_additive
(attr := simp) "If `a` semiconjugates `x` to `y` and `x'` to `y'`, then it semiconjugates `x + x'` to `y + y'`."] theorem
mul_right: SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')
mul_right
(
h: SemiconjBy a x y
h
:
SemiconjBy: {M : Type ?u.297} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: S
a
x: S
x
y: S
y
) (
h': SemiconjBy a x' y'
h'
:
SemiconjBy: {M : Type ?u.411} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: S
a
x': S
x'
y': S
y'
) :
SemiconjBy: {M : Type ?u.420} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: S
a
(
x: S
x
*
x': S
x'
) (
y: S
y
*
y': S
y'
) :=

Goals accomplished! 🐙
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


SemiconjBy a (x * x') (y * y')
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


SemiconjBy a (x * x') (y * y')
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * x * x' = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


y * a * x' = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


y * (a * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


y * (y' * a) = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


a * (x * x') = y * y' * a
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

h: SemiconjBy a x y

h': SemiconjBy a x' y'


y * y' * a = y * y' * a

Goals accomplished! 🐙
#align semiconj_by.mul_right
SemiconjBy.mul_right: ∀ {S : Type u_1} [inst : Semigroup S] {a x y x' y' : S}, SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')
SemiconjBy.mul_right
#align add_semiconj_by.add_right
AddSemiconjBy.add_right: ∀ {S : Type u_1} [inst : AddSemigroup S] {a x y x' y' : S}, AddSemiconjBy a x y → AddSemiconjBy a x' y' → AddSemiconjBy a (x + x') (y + y')
AddSemiconjBy.add_right
/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a * b` semiconjugates `x` to `z`. -/ @[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b x y z : S}, AddSemiconjBy a y z → AddSemiconjBy b x y → AddSemiconjBy (a + b) x z
to_additive
"If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a + b` semiconjugates `x` to `z`."] theorem
mul_left: SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
mul_left
(
ha: SemiconjBy a y z
ha
:
SemiconjBy: {M : Type ?u.1098} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: S
a
y: S
y
z: S
z
) (
hb: SemiconjBy b x y
hb
:
SemiconjBy: {M : Type ?u.1212} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
b: S
b
x: S
x
y: S
y
) :
SemiconjBy: {M : Type ?u.1221} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(
a: S
a
*
b: S
b
)
x: S
x
z: S
z
:=

Goals accomplished! 🐙
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


SemiconjBy (a * b) x z
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


SemiconjBy (a * b) x z
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * (b * x) = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * (y * b) = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * y * b = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


z * a * b = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


a * b * x = z * (a * b)
S: Type u_1

inst✝: Semigroup S

a, b, x, y, z, x', y': S

ha: SemiconjBy a y z

hb: SemiconjBy b x y


z * (a * b) = z * (a * b)

Goals accomplished! 🐙
#align semiconj_by.mul_left
SemiconjBy.mul_left: ∀ {S : Type u_1} [inst : Semigroup S] {a b x y z : S}, SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
SemiconjBy.mul_left
#align add_semiconj_by.add_left
AddSemiconjBy.add_left: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b x y z : S}, AddSemiconjBy a y z → AddSemiconjBy b x y → AddSemiconjBy (a + b) x z
AddSemiconjBy.add_left
/-- The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup is transitive. -/ @[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S], Transitive fun a b => ∃ c, AddSemiconjBy c a b
to_additive
"The relation “there exists an element that semiconjugates `a` to `b`” on an additive semigroup is transitive."] protected theorem
transitive: Transitive fun a b => ∃ c, SemiconjBy c a b
transitive
:
Transitive: {β : Sort ?u.1724} → (β → β → Prop) → Prop
Transitive
fun
a: S
a
b: S
b
:
S: ?m.1704
S
↦ ∃
c: ?m.1733
c
,
SemiconjBy: {M : Type ?u.1735} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
c: ?m.1733
c
a: S
a
b: S
b
|
_: S
_
,
_: S
_
,
_: S
_
, ⟨
x: S
x
,
hx: SemiconjBy x x✝² x✝¹
hx
⟩, ⟨
y: S
y
,
hy: SemiconjBy y x✝¹ x✝
hy
⟩ => ⟨
y: S
y
*
x: S
x
,
hy: SemiconjBy y x✝¹ x✝
hy
.
mul_left: ∀ {S : Type ?u.2180} [inst : Semigroup S] {a b x y z : S}, SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
mul_left
hx: SemiconjBy x x✝² x✝¹
hx
⟩ #align semiconj_by.transitive
SemiconjBy.transitive: ∀ {S : Type u_1} [inst : Semigroup S], Transitive fun a b => ∃ c, SemiconjBy c a b
SemiconjBy.transitive
#align add_semiconj_by.transitive
SemiconjBy.transitive: ∀ {S : Type u_1} [inst : Semigroup S], Transitive fun a b => ∃ c, SemiconjBy c a b
SemiconjBy.transitive
end Semigroup section MulOneClass variable [
MulOneClass: Type ?u.2905 → Type ?u.2905
MulOneClass
M: ?m.2605
M
] /-- Any element semiconjugates `1` to `1`. -/ @[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddSemiconjBy a 0 0
to_additive
(attr := simp) "Any element semiconjugates `0` to `0`."] theorem
one_right: ∀ {M : Type u_1} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
one_right
(
a: M
a
:
M: ?m.2605
M
) :
SemiconjBy: {M : Type ?u.2613} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
1: ?m.2621
1
1: ?m.2743
1
:=

Goals accomplished! 🐙
M: Type u_1

inst✝: MulOneClass M

a: M


M: Type u_1

inst✝: MulOneClass M

a: M


M: Type u_1

inst✝: MulOneClass M

a: M


a * 1 = 1 * a
M: Type u_1

inst✝: MulOneClass M

a: M


M: Type u_1

inst✝: MulOneClass M

a: M


a = 1 * a
M: Type u_1

inst✝: MulOneClass M

a: M


M: Type u_1

inst✝: MulOneClass M

a: M


a = a

Goals accomplished! 🐙
#align semiconj_by.one_right
SemiconjBy.one_right: ∀ {M : Type u_1} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
SemiconjBy.one_right
#align add_semiconj_by.zero_right
AddSemiconjBy.zero_right: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddSemiconjBy a 0 0
AddSemiconjBy.zero_right
/-- One semiconjugates any element to itself. -/ @[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), AddSemiconjBy 0 x x
to_additive
(attr := simp) "Zero semiconjugates any element to itself."] theorem
one_left: ∀ (x : M), SemiconjBy 1 x x
one_left
(
x: M
x
:
M: ?m.2902
M
) :
SemiconjBy: {M : Type ?u.2910} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
1: ?m.2918
1
x: M
x
x: M
x
:=
Eq.symm: ∀ {α : Sort ?u.3056} {a b : α}, a = b → b = a
Eq.symm
<|
one_right: ∀ {M : Type ?u.3063} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
one_right
x: M
x
#align semiconj_by.one_left
SemiconjBy.one_left: ∀ {M : Type u_1} [inst : MulOneClass M] (x : M), SemiconjBy 1 x x
SemiconjBy.one_left
#align add_semiconj_by.zero_left
AddSemiconjBy.zero_left: ∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), AddSemiconjBy 0 x x
AddSemiconjBy.zero_left
/-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more generally, on `MulOneClass` type) is reflexive. -/ @[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M], Reflexive fun a b => ∃ c, AddSemiconjBy c a b
to_additive
"The relation “there exists an element that semiconjugates `a` to `b`” on an additive monoid (or, more generally, on a `AddZeroClass` type) is reflexive."] protected theorem
reflexive: Reflexive fun a b => ∃ c, SemiconjBy c a b
reflexive
:
Reflexive: {β : Sort ?u.3130} → (β → β → Prop) → Prop
Reflexive
fun
a: M
a
b: M
b
:
M: ?m.3124
M
↦ ∃
c: ?m.3139
c
,
SemiconjBy: {M : Type ?u.3141} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
c: ?m.3139
c
a: M
a
b: M
b
|
a: ?m.3165
a
=> ⟨
1: ?m.3180
1
,
one_left: ∀ {M : Type ?u.3302} [inst : MulOneClass M] (x : M), SemiconjBy 1 x x
one_left
a: ?m.3165
a
⟩ #align semiconj_by.reflexive
SemiconjBy.reflexive: ∀ {M : Type u_1} [inst : MulOneClass M], Reflexive fun a b => ∃ c, SemiconjBy c a b
SemiconjBy.reflexive
#align add_semiconj_by.reflexive
AddSemiconjBy.reflexive: ∀ {M : Type u_1} [inst : AddZeroClass M], Reflexive fun a b => ∃ c, AddSemiconjBy c a b
AddSemiconjBy.reflexive
end MulOneClass section Monoid variable [
Monoid: Type ?u.7027 → Type ?u.7027
Monoid
M: ?m.7024
M
] /-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`. -/ @[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑x ↑y → AddSemiconjBy a ↑(-x) ↑(-y)
to_additive
"If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it semiconjugates `-x` to `-y`."] theorem
units_inv_right: ∀ {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
units_inv_right
{
a: M
a
:
M: ?m.3349
M
} {
x: MË£
x
y: MË£
y
:
M: ?m.3349
M
Ë£} (
h: SemiconjBy a ↑x ↑y
h
:
SemiconjBy: {M : Type ?u.3371} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
x: MË£
x
y: MË£
y
) :
SemiconjBy: {M : Type ?u.3626} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
↑
x: MË£
x
⁻¹ ↑
y: MË£
y
⁻¹ := calc
a: M
a
* ↑
x: MË£
x
⁻¹ = ↑
y: MË£
y
⁻¹ * (
y: MË£
y
*
a: M
a
) * ↑
x: MË£
x
⁻¹ :=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


a * ↑x⁻¹ = a * ↑x⁻¹

Goals accomplished! 🐙
_: ?m✝
_
= ↑
y: MË£
y
⁻¹ *
a: M
a
:=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (a * ↑x) * ↑x⁻¹ = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (a * ↑x * ↑x⁻¹) = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
M: Type u_1

inst✝: Monoid M

a: M

x, y: MË£

h: SemiconjBy a ↑x ↑y


↑y⁻¹ * a = ↑y⁻¹ * a

Goals accomplished! 🐙
#align semiconj_by.units_inv_right
SemiconjBy.units_inv_right: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
SemiconjBy.units_inv_right
#align add_semiconj_by.add_units_neg_right
AddSemiconjBy.addUnits_neg_right: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑x ↑y → AddSemiconjBy a ↑(-x) ↑(-y)
AddSemiconjBy.addUnits_neg_right
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑(-x) ↑(-y) ↔ AddSemiconjBy a ↑x ↑y
to_additive
(attr := simp)] theorem
units_inv_right_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
units_inv_right_iff
{
a: M
a
:
M: ?m.4802
M
} {
x: MË£
x
y: MË£
y
:
M: ?m.4802
M
Ë£} :
SemiconjBy: {M : Type ?u.4824} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
↑
x: MË£
x
⁻¹ ↑
y: MË£
y
⁻¹ ↔
SemiconjBy: {M : Type ?u.5088} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
x: MË£
x
y: MË£
y
:= ⟨
units_inv_right: ∀ {M : Type ?u.5305} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
units_inv_right
,
units_inv_right: ∀ {M : Type ?u.5339} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
units_inv_right
⟩ #align semiconj_by.units_inv_right_iff
SemiconjBy.units_inv_right_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
SemiconjBy.units_inv_right_iff
#align add_semiconj_by.add_units_neg_right_iff
AddSemiconjBy.addUnits_neg_right_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑(-x) ↑(-y) ↔ AddSemiconjBy a ↑x ↑y
AddSemiconjBy.addUnits_neg_right_iff
/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`. -/ @[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑a) x y → AddSemiconjBy (↑(-a)) y x
to_additive
"If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to `x`."] theorem
units_inv_symm_left: ∀ {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
units_inv_symm_left
{
a: MË£
a
:
M: ?m.5442
M
Ë£} {
x: M
x
y: M
y
:
M: ?m.5442
M
} (
h: SemiconjBy ?m.5469 x y
h
:
SemiconjBy: {M : Type ?u.5462} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(↑
a: MË£
a
)
x: M
x
y: M
y
) :
SemiconjBy: {M : Type ?u.5489} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(↑
a: MË£
a
⁻¹)
y: M
y
x: M
x
:= calc ↑
a: MË£
a
⁻¹ *
y: M
y
= ↑
a: MË£
a
⁻¹ * (
y: M
y
*
a: MË£
a
* ↑
a: MË£
a
⁻¹) :=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * y = ↑a⁻¹ * y

Goals accomplished! 🐙
_: ?m✝
_
=
x: M
x
* ↑
a: MË£
a
⁻¹ :=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (↑a * x * ↑a⁻¹) = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (↑a * x) * ↑a⁻¹ = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
M: Type u_1

inst✝: Monoid M

a: MË£

x, y: M

h: SemiconjBy (↑a) x y


x * ↑a⁻¹ = x * ↑a⁻¹

Goals accomplished! 🐙
#align semiconj_by.units_inv_symm_left
SemiconjBy.units_inv_symm_left: ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
SemiconjBy.units_inv_symm_left
#align add_semiconj_by.add_units_neg_symm_left
AddSemiconjBy.addUnits_neg_symm_left: ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑a) x y → AddSemiconjBy (↑(-a)) y x
AddSemiconjBy.addUnits_neg_symm_left
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑(-a)) y x ↔ AddSemiconjBy (↑a) x y
to_additive
(attr := simp)] theorem
units_inv_symm_left_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
units_inv_symm_left_iff
{
a: MË£
a
:
M: ?m.6589
M
Ë£} {
x: M
x
y: M
y
:
M: ?m.6589
M
} :
SemiconjBy: {M : Type ?u.6609} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(↑
a: MË£
a
⁻¹)
y: M
y
x: M
x
↔
SemiconjBy: {M : Type ?u.6630} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(↑
a: MË£
a
)
x: M
x
y: M
y
:= ⟨
units_inv_symm_left: ∀ {M : Type ?u.6887} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
units_inv_symm_left
,
units_inv_symm_left: ∀ {M : Type ?u.6921} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
units_inv_symm_left
⟩ #align semiconj_by.units_inv_symm_left_iff
SemiconjBy.units_inv_symm_left_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
SemiconjBy.units_inv_symm_left_iff
#align add_semiconj_by.add_units_neg_symm_left_iff
AddSemiconjBy.addUnits_neg_symm_left_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑(-a)) y x ↔ AddSemiconjBy (↑a) x y
AddSemiconjBy.addUnits_neg_symm_left_iff
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy a x y → AddSemiconjBy ↑a ↑x ↑y
to_additive
] theorem
units_val: ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy a x y → SemiconjBy ↑a ↑x ↑y
units_val
{
a: MË£
a
x: MË£
x
y: MË£
y
:
M: ?m.7024
M
Ë£} (
h: SemiconjBy a x y
h
:
SemiconjBy: {M : Type ?u.7048} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: MË£
a
x: MË£
x
y: MË£
y
) :
SemiconjBy: {M : Type ?u.7074} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(
a: MË£
a
:
M: ?m.7024
M
)
x: MË£
x
y: MË£
y
:=
congr_arg: ∀ {α : Sort ?u.7431} {β : Sort ?u.7430} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
Units.val: {α : Type ?u.7436} → [inst : Monoid α] → αˣ → α
Units.val
h: SemiconjBy a x y
h
#align semiconj_by.units_coe
SemiconjBy.units_val: ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy a x y → SemiconjBy ↑a ↑x ↑y
SemiconjBy.units_val
#align add_semiconj_by.add_units_coe
AddSemiconjBy.addUnits_val: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy a x y → AddSemiconjBy ↑a ↑x ↑y
AddSemiconjBy.addUnits_val
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y → AddSemiconjBy a x y
to_additive
] theorem
units_of_val: ∀ {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y → SemiconjBy a x y
units_of_val
{
a: MË£
a
x: MË£
x
y: MË£
y
:
M: ?m.7501
M
Ë£} (
h: SemiconjBy ↑a ↑x ↑y
h
:
SemiconjBy: {M : Type ?u.7525} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(
a: MË£
a
:
M: ?m.7501
M
)
x: MË£
x
y: MË£
y
) :
SemiconjBy: {M : Type ?u.7882} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: MË£
a
x: MË£
x
y: MË£
y
:=
Units.ext: ∀ {α : Type ?u.7907} [inst : Monoid α], Function.Injective Units.val
Units.ext
h: SemiconjBy ↑a ↑x ↑y
h
#align semiconj_by.units_of_coe
SemiconjBy.units_of_val: ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y → SemiconjBy a x y
SemiconjBy.units_of_val
#align add_semiconj_by.add_units_of_coe
AddSemiconjBy.addUnits_of_val: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y → AddSemiconjBy a x y
AddSemiconjBy.addUnits_of_val
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y ↔ AddSemiconjBy a x y
to_additive
(attr := simp)] theorem
units_val_iff: ∀ {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y
units_val_iff
{
a: MË£
a
x: MË£
x
y: MË£
y
:
M: ?m.7963
M
Ë£} :
SemiconjBy: {M : Type ?u.7987} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(
a: MË£
a
:
M: ?m.7963
M
)
x: MË£
x
y: MË£
y
↔
SemiconjBy: {M : Type ?u.8338} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: MË£
a
x: MË£
x
y: MË£
y
:= ⟨
units_of_val: ∀ {M : Type ?u.8362} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y → SemiconjBy a x y
units_of_val
,
units_val: ∀ {M : Type ?u.8396} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy a x y → SemiconjBy ↑a ↑x ↑y
units_val
⟩ #align semiconj_by.units_coe_iff
SemiconjBy.units_val_iff: ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y
SemiconjBy.units_val_iff
#align add_semiconj_by.add_units_coe_iff
AddSemiconjBy.addUnits_val_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y ↔ AddSemiconjBy a x y
AddSemiconjBy.addUnits_val_iff
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : M}, AddSemiconjBy a x y → ∀ (n : ℕ), AddSemiconjBy a (n • x) (n • y)
to_additive
(attr := simp)] theorem
pow_right: ∀ {a x y : M}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (x ^ n) (y ^ n)
pow_right
{
a: M
a
x: M
x
y: M
y
:
M: ?m.8491
M
} (
h: SemiconjBy a x y
h
:
SemiconjBy: {M : Type ?u.8503} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
x: M
x
y: M
y
) (n :
ℕ: Type
ℕ
) :
SemiconjBy: {M : Type ?u.8532} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
(
x: M
x
^ n) (
y: M
y
^ n) :=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ


SemiconjBy a (x ^ n) (y ^ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ


SemiconjBy a (x ^ n) (y ^ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y


zero

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ


SemiconjBy a (x ^ n) (y ^ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
SemiconjBy a (x * x ^ n) (y ^ Nat.succ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
SemiconjBy a (x * x ^ n) (y * y ^ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ
SemiconjBy a (x * x ^ n) (y * y ^ n)
M: Type u_1

inst✝: Monoid M

a, x, y: M

h: SemiconjBy a x y

n: ℕ

ih: SemiconjBy a (x ^ n) (y ^ n)


succ

Goals accomplished! 🐙
#align semiconj_by.pow_right
SemiconjBy.pow_right: ∀ {M : Type u_1} [inst : Monoid M] {a x y : M}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (x ^ n) (y ^ n)
SemiconjBy.pow_right
#align add_semiconj_by.nsmul_right
AddSemiconjBy.nsmul_right: ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : M}, AddSemiconjBy a x y → ∀ (n : ℕ), AddSemiconjBy a (n • x) (n • y)
AddSemiconjBy.nsmul_right
end Monoid section DivisionMonoid variable [
DivisionMonoid: Type ?u.9431 → Type ?u.9431
DivisionMonoid
G: ?m.9428
G
] {
a: G
a
x: G
x
y: G
y
:
G: ?m.9414
G
} @[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
to_additive
(attr := simp)] theorem inv_inv_symm_iff :
SemiconjBy: {M : Type ?u.9440} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
⁻¹
x: G
x
⁻¹
y: G
y
⁻¹ ↔
SemiconjBy: {M : Type ?u.9534} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
y: G
y
x: G
x
:=
inv_involutive: ∀ {G : Type ?u.9538} [inst : InvolutiveInv G], Function.Involutive Inv.inv
inv_involutive
.
injective: ∀ {α : Sort ?u.9549} {f : α → α}, Function.Involutive f → Function.Injective f
injective
.
eq_iff: ∀ {α : Sort ?u.9555} {β : Sort ?u.9556} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff
.
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans
<|

Goals accomplished! 🐙
G: Type u_1

inst✝: DivisionMonoid G

a, x, y: G


G: Type u_1

inst✝: DivisionMonoid G

a, x, y: G


x * a = a * y ↔ SemiconjBy a y x
G: Type u_1

inst✝: DivisionMonoid G

a, x, y: G


a * y = x * a ↔ SemiconjBy a y x
G: Type u_1

inst✝: DivisionMonoid G

a, x, y: G


a * y = x * a ↔ a * y = x * a

Goals accomplished! 🐙
#align semiconj_by.inv_inv_symm_iff
SemiconjBy.inv_inv_symm_iff: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
SemiconjBy.inv_inv_symm_iff
#align add_semiconj_by.neg_neg_symm_iff
AddSemiconjBy.neg_neg_symm_iff: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
AddSemiconjBy.neg_neg_symm_iff
@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy (-a) (-y) (-x)
to_additive
] theorem
inv_inv_symm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹
inv_inv_symm
:
SemiconjBy: {M : Type ?u.9947} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
y: G
y
→
SemiconjBy: {M : Type ?u.9993} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
⁻¹
y: G
y
⁻¹
x: G
x
⁻¹ :=
inv_inv_symm_iff: ∀ {G : Type ?u.10055} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
inv_inv_symm_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
#align semiconj_by.inv_inv_symm
SemiconjBy.inv_inv_symm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹
SemiconjBy.inv_inv_symm
#align add_semiconj_by.neg_neg_symm
AddSemiconjBy.neg_neg_symm: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy (-a) (-y) (-x)
AddSemiconjBy.neg_neg_symm
end DivisionMonoid section Group variable [
Group: Type ?u.10121 → Type ?u.10121
Group
G: ?m.10132
G
] {
a: G
a
x: G
x
y: G
y
:
G: ?m.10492
G
} @[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
to_additive
(attr := simp)] theorem inv_right_iff :
SemiconjBy: {M : Type ?u.10144} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
⁻¹
y: G
y
⁻¹ ↔
SemiconjBy: {M : Type ?u.10231} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
y: G
y
:= @
units_inv_right_iff: ∀ {M : Type ?u.10235} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
units_inv_right_iff
G: ?m.10132
G
_
a: G
a
⟨
x: G
x
,
x: G
x
⁻¹,
mul_inv_self: ∀ {G : Type ?u.10313} [inst : Group G] (a : G), a * a⁻¹ = 1
mul_inv_self
x: G
x
,
inv_mul_self: ∀ {G : Type ?u.10340} [inst : Group G] (a : G), a⁻¹ * a = 1
inv_mul_self
x: G
x
⟩ ⟨
y: G
y
,
y: G
y
⁻¹,
mul_inv_self: ∀ {G : Type ?u.10397} [inst : Group G] (a : G), a * a⁻¹ = 1
mul_inv_self
y: G
y
,
inv_mul_self: ∀ {G : Type ?u.10400} [inst : Group G] (a : G), a⁻¹ * a = 1
inv_mul_self
y: G
y
⟩ #align semiconj_by.inv_right_iff
SemiconjBy.inv_right_iff: ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
SemiconjBy.inv_right_iff
#align add_semiconj_by.neg_right_iff
AddSemiconjBy.neg_right_iff: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
AddSemiconjBy.neg_right_iff
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)
to_additive
] theorem
inv_right: SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
inv_right
:
SemiconjBy: {M : Type ?u.10505} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
y: G
y
→
SemiconjBy: {M : Type ?u.10543} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
⁻¹
y: G
y
⁻¹ :=
inv_right_iff: ∀ {G : Type ?u.10606} [inst : Group G] {a x y : G}, SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
inv_right_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
#align semiconj_by.inv_right
SemiconjBy.inv_right: ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
SemiconjBy.inv_right
#align add_semiconj_by.neg_right
AddSemiconjBy.neg_right: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)
AddSemiconjBy.neg_right
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
to_additive
(attr := simp)] theorem
inv_symm_left_iff: SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
inv_symm_left_iff
:
SemiconjBy: {M : Type ?u.10680} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
⁻¹
y: G
y
x: G
x
↔
SemiconjBy: {M : Type ?u.10756} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
y: G
y
:= @
units_inv_symm_left_iff: ∀ {M : Type ?u.10760} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
units_inv_symm_left_iff
G: ?m.10668
G
_ ⟨
a: G
a
,
a: G
a
⁻¹,
mul_inv_self: ∀ {G : Type ?u.10838} [inst : Group G] (a : G), a * a⁻¹ = 1
mul_inv_self
a: G
a
,
inv_mul_self: ∀ {G : Type ?u.10865} [inst : Group G] (a : G), a⁻¹ * a = 1
inv_mul_self
a: G
a
⟩
_: G
_
_: G
_
#align semiconj_by.inv_symm_left_iff
SemiconjBy.inv_symm_left_iff: ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
SemiconjBy.inv_symm_left_iff
#align add_semiconj_by.neg_symm_left_iff
AddSemiconjBy.neg_symm_left_iff: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
AddSemiconjBy.neg_symm_left_iff
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy (-a) y x
to_additive
] theorem
inv_symm_left: ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
inv_symm_left
:
SemiconjBy: {M : Type ?u.10988} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
y: G
y
→
SemiconjBy: {M : Type ?u.11026} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
⁻¹
y: G
y
x: G
x
:=
inv_symm_left_iff: ∀ {G : Type ?u.11078} [inst : Group G] {a x y : G}, SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
inv_symm_left_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
#align semiconj_by.inv_symm_left
SemiconjBy.inv_symm_left: ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
SemiconjBy.inv_symm_left
#align add_semiconj_by.neg_symm_left
AddSemiconjBy.neg_symm_left: ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy (-a) y x
AddSemiconjBy.neg_symm_left
/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ @[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] (a x : G), AddSemiconjBy a x (a + x + -a)
to_additive
"`a` semiconjugates `x` to `a + x + -a`."] theorem
conj_mk: ∀ {G : Type u_1} [inst : Group G] (a x : G), SemiconjBy a x (a * x * a⁻¹)
conj_mk
(
a: G
a
x: G
x
:
G: ?m.11140
G
) :
SemiconjBy: {M : Type ?u.11156} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: G
a
x: G
x
(
a: G
a
*
x: G
x
*
a: G
a
⁻¹) :=

Goals accomplished! 🐙
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * a⁻¹ * a
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * a⁻¹ * a
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * a⁻¹ * a
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * (a⁻¹ * a)
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * a⁻¹ * a
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * 1
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x * a⁻¹ * a
G: Type u_1

inst✝: Group G

a✝, x✝, y, a, x: G


a * x = a * x

Goals accomplished! 🐙
#align semiconj_by.conj_mk
SemiconjBy.conj_mk: ∀ {G : Type u_1} [inst : Group G] (a x : G), SemiconjBy a x (a * x * a⁻¹)
SemiconjBy.conj_mk
#align add_semiconj_by.conj_mk
AddSemiconjBy.conj_mk: ∀ {G : Type u_1} [inst : AddGroup G] (a x : G), AddSemiconjBy a x (a + x + -a)
AddSemiconjBy.conj_mk
end Group end SemiconjBy @[to_additive (attr := simp)
addSemiconjBy_iff_eq: ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a x y : M}, AddSemiconjBy a x y ↔ x = y
addSemiconjBy_iff_eq
] theorem
semiconjBy_iff_eq: ∀ {M : Type u_1} [inst : CancelCommMonoid M] {a x y : M}, SemiconjBy a x y ↔ x = y
semiconjBy_iff_eq
[
CancelCommMonoid: Type ?u.11593 → Type ?u.11593
CancelCommMonoid
M: ?m.11590
M
] {
a: M
a
x: M
x
y: M
y
:
M: ?m.11590
M
} :
SemiconjBy: {M : Type ?u.11602} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
a: M
a
x: M
x
y: M
y
↔
x: M
x
=
y: M
y
:= ⟨fun
h: ?m.11694
h
=>
mul_left_cancel: ∀ {G : Type ?u.11696} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel
(
h: ?m.11694
h
.
trans: ∀ {α : Sort ?u.11729} {a b c : α}, a = b → b = c → a = c
trans
(
mul_comm: ∀ {G : Type ?u.11749} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
_: ?m.11750
_
_: ?m.11750
_
)), fun
h: ?m.11895
h
=>

Goals accomplished! 🐙
M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


a * y = y * a
M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


M: Type u_1

inst✝: CancelCommMonoid M

a, x, y: M

h: x = y


y * a = y * a

Goals accomplished! 🐙
⟩ #align semiconj_by_iff_eq
semiconjBy_iff_eq: ∀ {M : Type u_1} [inst : CancelCommMonoid M] {a x y : M}, SemiconjBy a x y ↔ x = y
semiconjBy_iff_eq
#align add_semiconj_by_iff_eq
addSemiconjBy_iff_eq: ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a x y : M}, AddSemiconjBy a x y ↔ x = y
addSemiconjBy_iff_eq
/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ @[to_additive
AddUnits.mk_addSemiconjBy: ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M), AddSemiconjBy (↑u) x (↑u + x + ↑(-u))
AddUnits.mk_addSemiconjBy
"`a` semiconjugates `x` to `a + x + -a`."] theorem
Units.mk_semiconjBy: ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M), SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
Units.mk_semiconjBy
[
Monoid: Type ?u.12067 → Type ?u.12067
Monoid
M: ?m.12064
M
] (
u: MË£
u
:
M: ?m.12064
M
Ë£) (
x: M
x
:
M: ?m.12064
M
) :
SemiconjBy: {M : Type ?u.12082} → [inst : Mul M] → M → M → M → Prop
SemiconjBy
(↑
u: MË£
u
)
x: M
x
(
u: MË£
u
*
x: M
x
* ↑
u: MË£
u
⁻¹) :=

Goals accomplished! 🐙
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


↑u * x = ↑u * x * ↑u⁻¹ * ↑u
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


↑u * x = ↑u * x * ↑u⁻¹ * ↑u
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


↑u * x = ↑u * x * ↑u⁻¹ * ↑u
M: Type u_1

inst✝: Monoid M

u: MË£

x: M


↑u * x = ↑u * x

Goals accomplished! 🐙
#align units.mk_semiconj_by
Units.mk_semiconjBy: ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M), SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
Units.mk_semiconjBy
#align add_units.mk_semiconj_by
AddUnits.mk_addSemiconjBy: ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M), AddSemiconjBy (↑u) x (↑u + x + ↑(-u))
AddUnits.mk_addSemiconjBy