theorem AlgebraInLean.mul_left_eq {G : Type u_1} [AlgebraInLean.Group G] (a : G) (b : G) (c : G) (h : AlgebraInLean.μ a b = AlgebraInLean.μ a c) : b = c

theorem AlgebraInLean.inv_inj {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.Injective AlgebraInLean.ι

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

Equations

• AlgebraInLean.Homomorphism φ = ∀ (a b : G), AlgebraInLean.μ (φ a) (φ b) = φ (AlgebraInLean.μ a b)

theorem AlgebraInLean.Homomorphism_def {G : Type u_1} {H : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group H] (φ : G → H) : AlgebraInLean.Homomorphism φ ↔ ∀ (a b : G), AlgebraInLean.μ (φ a) (φ b) = φ (AlgebraInLean.μ a b)

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

Equations

• AlgebraInLean.Isomorphism φ = (AlgebraInLean.Homomorphism φ ∧ AlgebraInLean.Bijective φ)

theorem AlgebraInLean.hom_id_to_id {G : Type u_1} {H : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group H] (φ : G → H) (hp : AlgebraInLean.Homomorphism φ) : φ AlgebraInLean.𝕖 = AlgebraInLean.𝕖

theorem AlgebraInLean.two_sided_inv {G : Type u_1} [AlgebraInLean.Group G] (a : G) (b : G) (h1 : AlgebraInLean.μ a b = AlgebraInLean.𝕖) : b = AlgebraInLean.ι a

theorem AlgebraInLean.hom_inv_to_inv {G : Type u_1} {H : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group H] (φ : G → H) (hp : AlgebraInLean.Homomorphism φ) (g : G) : φ (AlgebraInLean.ι g) = AlgebraInLean.ι (φ g)