def AlgebraInLean.Endomorphism {G : Type u_1} [AlgebraInLean.Group G] (φ : G → G) : Prop

Equations

• AlgebraInLean.Endomorphism φ = AlgebraInLean.Homomorphism φ

def AlgebraInLean.Automorphism {G : Type u_1} [AlgebraInLean.Group G] (φ : G → G) : Prop

Equations

• AlgebraInLean.Automorphism φ = (AlgebraInLean.Endomorphism φ ∧ AlgebraInLean.Bijective φ)

theorem AlgebraInLean.aut_isomorphism {G : Type u_1} [AlgebraInLean.Group G] (φ : G → G) (h : AlgebraInLean.Automorphism φ) : AlgebraInLean.Isomorphism φ

def AlgebraInLean.int_neg (x : ℤ) : ℤ

Equations

• AlgebraInLean.int_neg x = -x

theorem AlgebraInLean.int_neg_automorphism (x : ℤ) (y : ℤ) : AlgebraInLean.int_neg (x + y) = AlgebraInLean.int_neg x + AlgebraInLean.int_neg y ∧ AlgebraInLean.Bijective AlgebraInLean.int_neg

def AlgebraInLean.conjugate {G : Type u_1} [AlgebraInLean.Group G] (g : G) (x : G) : G

Equations

• AlgebraInLean.conjugate g x = AlgebraInLean.μ (AlgebraInLean.μ g x) (AlgebraInLean.ι g)

theorem AlgebraInLean.conj_automorphism {G : Type u_1} [AlgebraInLean.Group G] (g : G) (x : G) (y : G) : AlgebraInLean.conjugate g (AlgebraInLean.μ x y) = AlgebraInLean.μ (AlgebraInLean.conjugate g x) (AlgebraInLean.conjugate g y) ∧ AlgebraInLean.Bijective (AlgebraInLean.conjugate g)