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: 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
! 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 β PropAddSemiconjBy "`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 β PropSemiconjBy [Mul: Type ?u.7 β Type ?u.7Mul M: ?m.4M] (a: Ma x: Mx y: My : M: ?m.4M) : Prop: TypeProp :=
a: Ma * x: Mx = y: My * a: Ma
#align semiconj_by SemiconjBy: {M : Type u_1} β [inst : Mul M] β M β M β M β PropSemiconjBy

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 + ato_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 * aeq [Mul: Type ?u.131 β Type ?u.131Mul S: ?m.128S] {a: Sa x: Sx y: Sy : S: ?m.128S} (h: SemiconjBy a x yh : SemiconjBy: {M : Type ?u.140} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa x: Sx y: Sy) : a: Sa * x: Sx = y: Sy * a: Sa :=
h: SemiconjBy a x yh
#align semiconj_by.eq SemiconjBy.eq: β {S : Type u_1} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aSemiconjBy.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 + aAddSemiconjBy.eq

section Semigroup

variable [Semigroup: Type ?u.1081 β Type ?u.1081Semigroup S: ?m.277S] {a: Sa b: Sb x: Sx y: Sy z: Sz x': Sx' y': Sy' : S: ?m.255S}

/-- 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 yh : SemiconjBy: {M : Type ?u.297} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa x: Sx y: Sy) (h': SemiconjBy a x' y'h' : SemiconjBy: {M : Type ?u.411} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa x': Sx' y': Sy') :
SemiconjBy: {M : Type ?u.420} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa (x: Sx * x': Sx') (y: Sy * y': Sy') := byGoals accomplished! π
S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'SemiconjBy a (x * x') (y * y')unfold SemiconjBy: {M : Type u_1} β [inst : Mul M] β M β M β M β PropSemiconjByS: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * a
-- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4
S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'SemiconjBy a (x * x') (y * y')rw [S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * aβmul_assoc: β {G : Type ?u.716} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * x * x' = y * y' * a S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * ah: SemiconjBy a x yh.eq: β {S : Type ?u.752} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'y * a * x' = y * y' * a S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * amul_assoc: β {G : Type ?u.877} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'y * (a * x') = y * y' * a S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * ah': SemiconjBy a x' y'h'.eq: β {S : Type ?u.900} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'y * (y' * a) = y * y' * a S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': SemiconjBy a x' y'a * (x * x') = y * y' * aβmul_assoc: β {G : Type ?u.915} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocS: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sh: SemiconjBy a x yh': 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

/-- 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 zto_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 zmul_left (ha: SemiconjBy a y zha : SemiconjBy: {M : Type ?u.1098} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa y: Sy z: Sz) (hb: SemiconjBy b x yhb : SemiconjBy: {M : Type ?u.1212} β [inst : Mul M] β M β M β M β PropSemiconjBy b: Sb x: Sx y: Sy) : SemiconjBy: {M : Type ?u.1221} β [inst : Mul M] β M β M β M β PropSemiconjBy (a: Sa * b: Sb) x: Sx z: Sz := byGoals accomplished! π
S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ySemiconjBy (a * b) x zunfold SemiconjBy: {M : Type u_1} β [inst : Mul M] β M β M β M β PropSemiconjByS: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)
S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ySemiconjBy (a * b) x zrw [S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)mul_assoc: β {G : Type ?u.1420} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * (b * x) = z * (a * b) S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)hb: SemiconjBy b x yhb.eq: β {S : Type ?u.1456} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * (y * b) = z * (a * b) S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)βmul_assoc: β {G : Type ?u.1581} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * y * b = z * (a * b) S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)ha: SemiconjBy a y zha.eq: β {S : Type ?u.1604} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x yz * a * b = z * (a * b) S: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x ya * b * x = z * (a * b)mul_assoc: β {G : Type ?u.1619} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocS: Type u_1instβ: Semigroup Sa, b, x, y, z, x', y': Sha: SemiconjBy a y zhb: SemiconjBy b x yz * (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 zSemiconjBy.mul_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 bto_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 btransitive : Transitive: {Ξ² : Sort ?u.1724} β (Ξ² β Ξ² β Prop) β PropTransitive fun a: Sa b: Sb : S: ?m.1704S β¦ β c: ?m.1733c, SemiconjBy: {M : Type ?u.1735} β [inst : Mul M] β M β M β M β PropSemiconjBy c: ?m.1733c a: Sa b: Sb
| _: S_, _: S_, _: S_, β¨x: Sx, hx: SemiconjBy x xβΒ² xβΒΉhxβ©, β¨y: Sy, hy: SemiconjBy y xβΒΉ xβhyβ© => β¨y: Sy * x: Sx, 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 zmul_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 bSemiconjBy.transitive
#align add_semiconj_by.transitive SemiconjBy.transitive: β {S : Type u_1} [inst : Semigroup S], Transitive fun a b => β c, SemiconjBy c a bSemiconjBy.transitive

end Semigroup

section MulOneClass

variable [MulOneClass: Type ?u.2905 β Type ?u.2905MulOneClass M: ?m.2605M]

/-- Any element semiconjugates `1` to `1`. -/
@[to_additive: β {M : Type u_1} [inst : AddZeroClass M] (a : M), AddSemiconjBy a 0 0to_additive (attr := simp) "Any element semiconjugates `0` to `0`."]
theorem one_right: β {M : Type u_1} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1one_right (a: Ma : M: ?m.2605M) : SemiconjBy: {M : Type ?u.2613} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma 1: ?m.26211 1: ?m.27431 := byGoals accomplished! π M: Type u_1instβ: MulOneClass Ma: MSemiconjBy a 1 1rw [M: Type u_1instβ: MulOneClass Ma: MSemiconjBy a 1 1SemiconjBy: {M : Type ?u.2792} β [inst : Mul M] β M β M β M β PropSemiconjBy,M: Type u_1instβ: MulOneClass Ma: Ma * 1 = 1 * a M: Type u_1instβ: MulOneClass Ma: MSemiconjBy a 1 1mul_one: β {M : Type ?u.2793} [inst : MulOneClass M] (a : M), a * 1 = amul_one,M: Type u_1instβ: MulOneClass Ma: Ma = 1 * a M: Type u_1instβ: MulOneClass Ma: MSemiconjBy a 1 1one_mul: β {M : Type ?u.2823} [inst : MulOneClass M] (a : M), 1 * a = aone_mulM: Type u_1instβ: MulOneClass Ma: Ma = a]Goals accomplished! π
#align semiconj_by.one_right SemiconjBy.one_right: β {M : Type u_1} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1SemiconjBy.one_right

/-- One semiconjugates any element to itself. -/
@[to_additive: β {M : Type u_1} [inst : AddZeroClass M] (x : M), AddSemiconjBy 0 x xto_additive (attr := simp) "Zero semiconjugates any element to itself."]
theorem one_left: β (x : M), SemiconjBy 1 x xone_left (x: Mx : M: ?m.2902M) : SemiconjBy: {M : Type ?u.2910} β [inst : Mul M] β M β M β M β PropSemiconjBy 1: ?m.29181 x: Mx x: Mx :=
Eq.symm: β {Ξ± : Sort ?u.3056} {a b : Ξ±}, a = b β b = aEq.symm <| one_right: β {M : Type ?u.3063} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1one_right x: Mx
#align semiconj_by.one_left SemiconjBy.one_left: β {M : Type u_1} [inst : MulOneClass M] (x : M), SemiconjBy 1 x xSemiconjBy.one_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 bto_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 breflexive : Reflexive: {Ξ² : Sort ?u.3130} β (Ξ² β Ξ² β Prop) β PropReflexive fun a: Ma b: Mb : M: ?m.3124M β¦ β c: ?m.3139c, SemiconjBy: {M : Type ?u.3141} β [inst : Mul M] β M β M β M β PropSemiconjBy c: ?m.3139c a: Ma b: Mb
| a: ?m.3165a => β¨1: ?m.31801, one_left: β {M : Type ?u.3302} [inst : MulOneClass M] (x : M), SemiconjBy 1 x xone_left a: ?m.3165aβ©
#align semiconj_by.reflexive SemiconjBy.reflexive: β {M : Type u_1} [inst : MulOneClass M], Reflexive fun a b => β c, SemiconjBy c a bSemiconjBy.reflexive

end MulOneClass

section Monoid

variable [Monoid: Type ?u.7027 β Type ?u.7027Monoid M: ?m.7024M]

/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `xβ»ΒΉ` to `yβ»ΒΉ`. -/
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: Ma : M: ?m.3349M} {x: MΛ£x y: MΛ£y : M: ?m.3349MΛ£} (h: SemiconjBy a βx βyh : SemiconjBy: {M : Type ?u.3371} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma x: MΛ£x y: MΛ£y) : SemiconjBy: {M : Type ?u.3626} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma βx: MΛ£xβ»ΒΉ βy: MΛ£yβ»ΒΉ :=
calc
a: Ma * βx: MΛ£xβ»ΒΉ = βy: MΛ£yβ»ΒΉ * (y: MΛ£y * a: Ma) * βx: MΛ£xβ»ΒΉ := byGoals accomplished! π M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βya * βxβ»ΒΉ = βyβ»ΒΉ * (βy * a) * βxβ»ΒΉrw [M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βya * βxβ»ΒΉ = βyβ»ΒΉ * (βy * a) * βxβ»ΒΉUnits.inv_mul_cancel_left: β {Ξ± : Type ?u.4589} [inst : Monoid Ξ±] (a : Ξ±Λ£) (b : Ξ±), βaβ»ΒΉ * (βa * b) = bUnits.inv_mul_cancel_leftM: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βya * βxβ»ΒΉ = a * βxβ»ΒΉ]Goals accomplished! π
_: ?mβ_        = βy: MΛ£yβ»ΒΉ * a: Ma              := byGoals accomplished! π M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (βy * a) * βxβ»ΒΉ = βyβ»ΒΉ * arw [M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (βy * a) * βxβ»ΒΉ = βyβ»ΒΉ * aβ h: SemiconjBy a βx βyh.eq: β {S : Type ?u.4644} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (a * βx) * βxβ»ΒΉ = βyβ»ΒΉ * a M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (βy * a) * βxβ»ΒΉ = βyβ»ΒΉ * amul_assoc: β {G : Type ?u.4676} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (a * βx * βxβ»ΒΉ) = βyβ»ΒΉ * a M: Type u_1instβ: Monoid Ma: Mx, y: MΛ£h: SemiconjBy a βx βyβyβ»ΒΉ * (βy * a) * βxβ»ΒΉ = βyβ»ΒΉ * aUnits.mul_inv_cancel_right: β {Ξ± : Type ?u.4724} [inst : Monoid Ξ±] (a : Ξ±) (b : Ξ±Λ£), a * βb * βbβ»ΒΉ = aUnits.mul_inv_cancel_rightM: Type u_1instβ: Monoid Ma: Mx, 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

theorem units_inv_right_iff: β {M : Type u_1} [inst : Monoid M] {a : M} {x y : MΛ£}, SemiconjBy a βxβ»ΒΉ βyβ»ΒΉ β SemiconjBy a βx βyunits_inv_right_iff {a: Ma : M: ?m.4802M} {x: MΛ£x y: MΛ£y : M: ?m.4802MΛ£} : SemiconjBy: {M : Type ?u.4824} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma βx: MΛ£xβ»ΒΉ βy: MΛ£yβ»ΒΉ β SemiconjBy: {M : Type ?u.5088} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma 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 βySemiconjBy.units_inv_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 xto_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 xunits_inv_symm_left {a: MΛ£a : M: ?m.5442MΛ£} {x: Mx y: My : M: ?m.5442M} (h: SemiconjBy ?m.5469 x yh : SemiconjBy: {M : Type ?u.5462} β [inst : Mul M] β M β M β M β PropSemiconjBy (βa: MΛ£a) x: Mx y: My) : SemiconjBy: {M : Type ?u.5489} β [inst : Mul M] β M β M β M β PropSemiconjBy (βa: MΛ£aβ»ΒΉ) y: My x: Mx :=
calc
βa: MΛ£aβ»ΒΉ * y: My = βa: MΛ£aβ»ΒΉ * (y: My * a: MΛ£a * βa: MΛ£aβ»ΒΉ) := byGoals accomplished! π M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * y = βaβ»ΒΉ * (y * βa * βaβ»ΒΉ)rw [M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * y = βaβ»ΒΉ * (y * βa * βaβ»ΒΉ)Units.mul_inv_cancel_right: β {Ξ± : Type ?u.6376} [inst : Monoid Ξ±] (a : Ξ±) (b : Ξ±Λ£), a * βb * βbβ»ΒΉ = aUnits.mul_inv_cancel_rightM: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * y = βaβ»ΒΉ * y]Goals accomplished! π
_: ?mβ_ = x: Mx * βa: MΛ£aβ»ΒΉ := byGoals accomplished! π M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (y * βa * βaβ»ΒΉ) = x * βaβ»ΒΉrw [M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (y * βa * βaβ»ΒΉ) = x * βaβ»ΒΉβ h: SemiconjBy (βa) x yh.eq: β {S : Type ?u.6431} [inst : Mul S] {a x y : S}, SemiconjBy a x y β a * x = y * aeq,M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (βa * x * βaβ»ΒΉ) = x * βaβ»ΒΉ M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (y * βa * βaβ»ΒΉ) = x * βaβ»ΒΉβ mul_assoc: β {G : Type ?u.6463} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (βa * x) * βaβ»ΒΉ = x * βaβ»ΒΉ M: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yβaβ»ΒΉ * (y * βa * βaβ»ΒΉ) = x * βaβ»ΒΉUnits.inv_mul_cancel_left: β {Ξ± : Type ?u.6511} [inst : Monoid Ξ±] (a : Ξ±Λ£) (b : Ξ±), βaβ»ΒΉ * (βa * b) = bUnits.inv_mul_cancel_leftM: Type u_1instβ: Monoid Ma: MΛ£x, y: Mh: SemiconjBy (βa) x yx * β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 xSemiconjBy.units_inv_symm_left

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 yunits_inv_symm_left_iff {a: MΛ£a : M: ?m.6589MΛ£} {x: Mx y: My : M: ?m.6589M} : SemiconjBy: {M : Type ?u.6609} β [inst : Mul M] β M β M β M β PropSemiconjBy (βa: MΛ£aβ»ΒΉ) y: My x: Mx β SemiconjBy: {M : Type ?u.6630} β [inst : Mul M] β M β M β M β PropSemiconjBy (βa: MΛ£a) x: Mx y: My :=
β¨units_inv_symm_left: β {M : Type ?u.6887} [inst : Monoid M] {a : MΛ£} {x y : M}, SemiconjBy (βa) x y β SemiconjBy (βaβ»ΒΉ) y xunits_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 xunits_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 ySemiconjBy.units_inv_symm_left_iff

theorem units_val: β {M : Type u_1} [inst : Monoid M] {a x y : MΛ£}, SemiconjBy a x y β SemiconjBy βa βx βyunits_val {a: MΛ£a x: MΛ£x y: MΛ£y : M: ?m.7024MΛ£} (h: SemiconjBy a x yh : SemiconjBy: {M : Type ?u.7048} β [inst : Mul M] β M β M β M β PropSemiconjBy a: MΛ£a x: MΛ£x y: MΛ£y) : SemiconjBy: {M : Type ?u.7074} β [inst : Mul M] β M β M β M β PropSemiconjBy (a: MΛ£a : M: ?m.7024M) 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 yh
#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 βySemiconjBy.units_val

theorem units_of_val: β {a x y : MΛ£}, SemiconjBy βa βx βy β SemiconjBy a x yunits_of_val {a: MΛ£a x: MΛ£x y: MΛ£y : M: ?m.7501MΛ£} (h: SemiconjBy βa βx βyh : SemiconjBy: {M : Type ?u.7525} β [inst : Mul M] β M β M β M β PropSemiconjBy (a: MΛ£a : M: ?m.7501M) x: MΛ£x y: MΛ£y) : SemiconjBy: {M : Type ?u.7882} β [inst : Mul M] β M β M β M β PropSemiconjBy a: MΛ£a x: MΛ£x y: MΛ£y :=
Units.ext: β {Ξ± : Type ?u.7907} [inst : Monoid Ξ±], Function.Injective Units.valUnits.ext h: SemiconjBy βa βx βyh
#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 ySemiconjBy.units_of_val

theorem units_val_iff: β {a x y : MΛ£}, SemiconjBy βa βx βy β SemiconjBy a x yunits_val_iff {a: MΛ£a x: MΛ£x y: MΛ£y : M: ?m.7963MΛ£} : SemiconjBy: {M : Type ?u.7987} β [inst : Mul M] β M β M β M β PropSemiconjBy (a: MΛ£a : M: ?m.7963M) x: MΛ£x y: MΛ£y β SemiconjBy: {M : Type ?u.8338} β [inst : Mul M] β M β M β M β PropSemiconjBy 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 yunits_of_val, units_val: β {M : Type ?u.8396} [inst : Monoid M] {a x y : MΛ£}, SemiconjBy a x y β SemiconjBy βa βx βyunits_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 ySemiconjBy.units_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: Ma x: Mx y: My : M: ?m.8491M} (h: SemiconjBy a x yh : SemiconjBy: {M : Type ?u.8503} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma x: Mx y: My) (n: βn : β: Typeβ) : SemiconjBy: {M : Type ?u.8532} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ma (x: Mx ^ n: βn) (y: My ^ n: βn) := byGoals accomplished! π
M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βSemiconjBy a (x ^ n) (y ^ n)induction' n: βn with n: βn ih: ?m.9095 nihM: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)
M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βSemiconjBy a (x ^ n) (y ^ n)Β·M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero) M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)rw [M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)pow_zero: β {M : Type ?u.9106} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a 1 (y ^ Nat.zero) M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)pow_zero: β {M : Type ?u.9142} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zeroM: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a 1 1]M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a 1 1
M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yzeroSemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)exact SemiconjBy.one_right: β {M : Type ?u.9165} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1SemiconjBy.one_right _: ?m.9166_Goals accomplished! π
M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βSemiconjBy a (x ^ n) (y ^ n)Β·M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n) M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)rw [M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)pow_succ: β {M : Type ?u.9197} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_succ,M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x * x ^ n) (y ^ Nat.succ n) M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)pow_succ: β {M : Type ?u.9218} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_succM: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x * x ^ n) (y * y ^ n)]M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x * x ^ n) (y * y ^ n)
M: Type u_1instβ: Monoid Ma, x, y: Mh: SemiconjBy a x yn: βih: SemiconjBy a (x ^ n) (y ^ n)succSemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)exact h: SemiconjBy a x yh.mul_right: β {S : Type ?u.9255} [inst : Semigroup S] {a x y x' y' : S},
SemiconjBy a x y β SemiconjBy a x' y' β SemiconjBy a (x * x') (y * y')mul_right ih: ?m.9095 nihGoals 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.9431DivisionMonoid G: ?m.9428G] {a: Ga x: Gx y: Gy : G: ?m.9414G}

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy (-a) (-x) (-y) β AddSemiconjBy a y xto_additive (attr := simp)]
theorem inv_inv_symm_iff: SemiconjBy aβ»ΒΉ xβ»ΒΉ yβ»ΒΉ β SemiconjBy a y xinv_inv_symm_iff : SemiconjBy: {M : Type ?u.9440} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Gaβ»ΒΉ x: Gxβ»ΒΉ y: Gyβ»ΒΉ β SemiconjBy: {M : Type ?u.9534} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga y: Gy x: Gx :=
inv_involutive: β {G : Type ?u.9538} [inst : InvolutiveInv G], Function.Involutive Inv.invinv_involutive.injective: β {Ξ± : Sort ?u.9549} {f : Ξ± β Ξ±}, Function.Involutive f β Function.Injective finjective.eq_iff: β {Ξ± : Sort ?u.9555} {Ξ² : Sort ?u.9556} {f : Ξ± β Ξ²}, Function.Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff.symm: β {a b : Prop}, (a β b) β (b β a)symm.trans: β {a b c : Prop}, (a β b) β (b β c) β (a β c)trans <| byGoals accomplished! π
G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xrw [G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xmul_inv_rev: β {G : Type ?u.9594} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_rev,G: Type u_1instβ: DivisionMonoid Ga, x, y: Gxβ»ΒΉβ»ΒΉ * aβ»ΒΉβ»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xmul_inv_rev: β {G : Type ?u.9635} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_rev,G: Type u_1instβ: DivisionMonoid Ga, x, y: Gxβ»ΒΉβ»ΒΉ * aβ»ΒΉβ»ΒΉ = aβ»ΒΉβ»ΒΉ * yβ»ΒΉβ»ΒΉ β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xinv_inv: β {G : Type ?u.9689} [inst : InvolutiveInv G] (a : G), aβ»ΒΉβ»ΒΉ = ainv_inv,G: Type u_1instβ: DivisionMonoid Ga, x, y: Gx * aβ»ΒΉβ»ΒΉ = aβ»ΒΉβ»ΒΉ * yβ»ΒΉβ»ΒΉ β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xinv_inv: β {G : Type ?u.9713} [inst : InvolutiveInv G] (a : G), aβ»ΒΉβ»ΒΉ = ainv_inv,G: Type u_1instβ: DivisionMonoid Ga, x, y: Gx * a = a * yβ»ΒΉβ»ΒΉ β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xinv_inv: β {G : Type ?u.9737} [inst : InvolutiveInv G] (a : G), aβ»ΒΉβ»ΒΉ = ainv_inv,G: Type u_1instβ: DivisionMonoid Ga, x, y: Gx * a = a * y β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xeq_comm: β {Ξ± : Sort ?u.9761} {a b : Ξ±}, a = b β b = aeq_comm,G: Type u_1instβ: DivisionMonoid Ga, x, y: Ga * y = x * a β SemiconjBy a y x G: Type u_1instβ: DivisionMonoid Ga, x, y: G(aβ»ΒΉ * xβ»ΒΉ)β»ΒΉ = (yβ»ΒΉ * aβ»ΒΉ)β»ΒΉ β SemiconjBy a y xSemiconjBy: {M : Type ?u.9831} β [inst : Mul M] β M β M β M β PropSemiconjByG: Type u_1instβ: DivisionMonoid Ga, x, y: Ga * 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 xSemiconjBy.inv_inv_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 β PropSemiconjBy a: Ga x: Gx y: Gy β SemiconjBy: {M : Type ?u.9993} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Gaβ»ΒΉ y: Gyβ»ΒΉ x: Gxβ»ΒΉ :=
inv_inv_symm_iff: β {G : Type ?u.10055} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy aβ»ΒΉ xβ»ΒΉ yβ»ΒΉ β SemiconjBy a y xinv_inv_symm_iff.2: β {a b : Prop}, (a β b) β b β a2
#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

end DivisionMonoid

section Group

variable [Group: Type ?u.10121 β Type ?u.10121Group G: ?m.10132G] {a: Ga x: Gx y: Gy : G: ?m.10492G}

theorem inv_right_iff: SemiconjBy a xβ»ΒΉ yβ»ΒΉ β SemiconjBy a x yinv_right_iff : SemiconjBy: {M : Type ?u.10144} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gxβ»ΒΉ y: Gyβ»ΒΉ β SemiconjBy: {M : Type ?u.10231} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gx y: Gy :=
@units_inv_right_iff: β {M : Type ?u.10235} [inst : Monoid M] {a : M} {x y : MΛ£}, SemiconjBy a βxβ»ΒΉ βyβ»ΒΉ β SemiconjBy a βx βyunits_inv_right_iff G: ?m.10132G _ a: Ga β¨x: Gx, x: Gxβ»ΒΉ, mul_inv_self: β {G : Type ?u.10313} [inst : Group G] (a : G), a * aβ»ΒΉ = 1mul_inv_self x: Gx, inv_mul_self: β {G : Type ?u.10340} [inst : Group G] (a : G), aβ»ΒΉ * a = 1inv_mul_self x: Gxβ©
β¨y: Gy, y: Gyβ»ΒΉ, mul_inv_self: β {G : Type ?u.10397} [inst : Group G] (a : G), a * aβ»ΒΉ = 1mul_inv_self y: Gy, inv_mul_self: β {G : Type ?u.10400} [inst : Group G] (a : G), aβ»ΒΉ * a = 1inv_mul_self y: Gyβ©
#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 ySemiconjBy.inv_right_iff

theorem inv_right: SemiconjBy a x y β SemiconjBy a xβ»ΒΉ yβ»ΒΉinv_right : SemiconjBy: {M : Type ?u.10505} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gx y: Gy β SemiconjBy: {M : Type ?u.10543} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gxβ»ΒΉ y: Gyβ»ΒΉ :=
inv_right_iff: β {G : Type ?u.10606} [inst : Group G] {a x y : G}, SemiconjBy a xβ»ΒΉ yβ»ΒΉ β SemiconjBy a x yinv_right_iff.2: β {a b : Prop}, (a β b) β b β a2
#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

theorem inv_symm_left_iff: SemiconjBy aβ»ΒΉ y x β SemiconjBy a x yinv_symm_left_iff : SemiconjBy: {M : Type ?u.10680} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Gaβ»ΒΉ y: Gy x: Gx β SemiconjBy: {M : Type ?u.10756} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gx y: Gy :=
@units_inv_symm_left_iff: β {M : Type ?u.10760} [inst : Monoid M] {a : MΛ£} {x y : M}, SemiconjBy (βaβ»ΒΉ) y x β SemiconjBy (βa) x yunits_inv_symm_left_iff G: ?m.10668G _ β¨a: Ga, a: Gaβ»ΒΉ, mul_inv_self: β {G : Type ?u.10838} [inst : Group G] (a : G), a * aβ»ΒΉ = 1mul_inv_self a: Ga, inv_mul_self: β {G : Type ?u.10865} [inst : Group G] (a : G), aβ»ΒΉ * a = 1inv_mul_self a: Gaβ© _: 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 ySemiconjBy.inv_symm_left_iff

theorem inv_symm_left: β {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y β SemiconjBy aβ»ΒΉ y xinv_symm_left : SemiconjBy: {M : Type ?u.10988} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gx y: Gy β SemiconjBy: {M : Type ?u.11026} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Gaβ»ΒΉ y: Gy x: Gx :=
inv_symm_left_iff: β {G : Type ?u.11078} [inst : Group G] {a x y : G}, SemiconjBy aβ»ΒΉ y x β SemiconjBy a x yinv_symm_left_iff.2: β {a b : Prop}, (a β b) β b β a2
#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 xSemiconjBy.inv_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: Ga x: Gx : G: ?m.11140G) : SemiconjBy: {M : Type ?u.11156} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Ga x: Gx (a: Ga * x: Gx * a: Gaβ»ΒΉ) := byGoals accomplished! π
G: Type u_1instβ: Group Gaβ, xβ, y, a, x: GSemiconjBy a x (a * x * aβ»ΒΉ)unfold SemiconjBy: {M : Type u_1} β [inst : Mul M] β M β M β M β PropSemiconjByG: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * aβ»ΒΉ * a;G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * aβ»ΒΉ * a G: Type u_1instβ: Group Gaβ, xβ, y, a, x: GSemiconjBy a x (a * x * aβ»ΒΉ)rw [G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * aβ»ΒΉ * amul_assoc: β {G : Type ?u.11346} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * (aβ»ΒΉ * a) G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * aβ»ΒΉ * ainv_mul_self: β {G : Type ?u.11450} [inst : Group G] (a : G), aβ»ΒΉ * a = 1inv_mul_self,G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * 1 G: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * x = a * x * aβ»ΒΉ * amul_one: β {M : Type ?u.11507} [inst : MulOneClass M] (a : M), a * 1 = amul_oneG: Type u_1instβ: Group Gaβ, xβ, y, a, x: Ga * 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

end Group

end SemiconjBy