# Additional lemmas about monoid and group homomorphisms #

source
def powMonoidHom {α : Type u_1} [CommMonoid α] (n : ℕ) :
α →* α

The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of monoids.

Equations

- powMonoidHom n = { toFun := fun (x : α) => x ^ n, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def nsmulAddMonoidHom {α : Type u_1} [AddCommMonoid α] (n : ℕ) :
α →+ α

Multiplication by a natural `n` on a commutative additive monoid, considered as a morphism of additive monoids.

Equations

- nsmulAddMonoidHom n = { toFun := fun (x : α) => n • x, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem powMonoidHom_apply {α : Type u_1} [CommMonoid α] (n : ℕ) (x✝ : α) :
(powMonoidHom n) x✝ = x✝ ^ n
source
@[simp]
theorem nsmulAddMonoidHom_apply {α : Type u_1} [AddCommMonoid α] (n : ℕ) (x✝ : α) :
(nsmulAddMonoidHom n) x✝ = n • x✝
source
def zpowGroupHom {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) :
α →* α

The `n`-th power map (for an integer `n`) on a commutative group, considered as a group homomorphism.

Equations

- zpowGroupHom n = { toFun := fun (x : α) => x ^ n, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def zsmulAddGroupHom {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) :
α →+ α

Multiplication by an integer `n` on a commutative additive group, considered as an additive group homomorphism.

Equations

- zsmulAddGroupHom n = { toFun := fun (x : α) => n • x, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem zsmulAddGroupHom_apply {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) (x✝ : α) :
(zsmulAddGroupHom n) x✝ = n • x✝
source
@[simp]
theorem zpowGroupHom_apply {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) (x✝ : α) :
(zpowGroupHom n) x✝ = x✝ ^ n
source
def invMonoidHom {α : Type u_1} [DivisionCommMonoid α] :
α →* α

Inversion on a commutative group, considered as a monoid homomorphism.

Equations

- invMonoidHom = { toFun := Inv.inv, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def negAddMonoidHom {α : Type u_1} [SubtractionCommMonoid α] :
α →+ α

Negation on a commutative additive group, considered as an additive monoid homomorphism.

Equations

- negAddMonoidHom = { toFun := Neg.neg, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem coe_invMonoidHom {α : Type u_1} [DivisionCommMonoid α] :
⇑invMonoidHom = Inv.inv
source
@[simp]
theorem invMonoidHom_apply {α : Type u_1} [DivisionCommMonoid α] (a : α) :
invMonoidHom a = a⁻¹
source
instance OneHom.instMul {M : Type u_2} {N : Type u_3} [One M] [MulOneClass N] :
Mul (OneHom M N)

Given two one-preserving morphisms `f`, `g`, `f * g` is the one-preserving morphism sending `x` to `f x * g x`.

Equations

- OneHom.instMul = { mul := fun (f g : OneHom M N) => { toFun := fun (m : M) => f m * g m, map_one' := ⋯ } }

source
instance ZeroHom.instAdd {M : Type u_2} {N : Type u_3} [Zero M] [AddZeroClass N] :
Add (ZeroHom M N)

Given two zero-preserving morphisms `f`, `g`, `f + g` is the zero-preserving morphism sending `x` to `f x + g x`.

Equations

- ZeroHom.instAdd = { add := fun (f g : ZeroHom M N) => { toFun := fun (m : M) => f m + g m, map_zero' := ⋯ } }

source
theorem OneHom.coe_mul {M : Type u_8} {N : Type u_9} [One M] [MulOneClass N] (f g : OneHom M N) :
⇑(f * g) = ⇑f * ⇑g
source
theorem ZeroHom.coe_add {M : Type u_8} {N : Type u_9} [Zero M] [AddZeroClass N] (f g : ZeroHom M N) :
⇑(f + g) = ⇑f + ⇑g
source
@[simp]
theorem OneHom.mul_apply {M : Type u_8} {N : Type u_9} [One M] [MulOneClass N] (f g : OneHom M N) (x : M) :
(f * g) x = f x * g x
source
@[simp]
theorem ZeroHom.add_apply {M : Type u_8} {N : Type u_9} [Zero M] [AddZeroClass N] (f g : ZeroHom M N) (x : M) :
(f + g) x = f x + g x
source
theorem OneHom.mul_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [One M] [One N] [MulOneClass P] (g₁ g₂ : OneHom N P) (f : OneHom M N) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
source
theorem ZeroHom.add_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Zero M] [Zero N] [AddZeroClass P] (g₁ g₂ : ZeroHom N P) (f : ZeroHom M N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
source
instance OneHom.instInv {M : Type u_2} {N : Type u_3} [One M] [InvOneClass N] :
Inv (OneHom M N)

Given a one-preserving morphism `f`, `f⁻¹` is the one-preserving morphism sending `x` to `(f x)⁻¹`.

Equations

- OneHom.instInv = { inv := fun (f : OneHom M N) => { toFun := fun (m : M) => (f m)⁻¹, map_one' := ⋯ } }

source
instance ZeroHom.instNeg {M : Type u_2} {N : Type u_3} [Zero M] [NegZeroClass N] :
Neg (ZeroHom M N)

Given a zero-preserving morphism `f`, `-f` is the zero-preserving morphism sending `x` to `-f x`.

Equations

- ZeroHom.instNeg = { neg := fun (f : ZeroHom M N) => { toFun := fun (m : M) => -f m, map_zero' := ⋯ } }

source
theorem OneHom.coe_inv {M : Type u_8} {N : Type u_9} [One M] [InvOneClass N] (f : OneHom M N) :
⇑f⁻¹ = (⇑f)⁻¹
source
theorem ZeroHom.coe_neg {M : Type u_8} {N : Type u_9} [Zero M] [NegZeroClass N] (f : ZeroHom M N) :
⇑(-f) = -⇑f
source
@[simp]
theorem OneHom.inv_apply {M : Type u_8} {N : Type u_9} [One M] [InvOneClass N] (f : OneHom M N) (x : M) :
f⁻¹ x = (f x)⁻¹
source
@[simp]
theorem ZeroHom.neg_apply {M : Type u_8} {N : Type u_9} [Zero M] [NegZeroClass N] (f : ZeroHom M N) (x : M) :
(-f) x = -f x
source
theorem OneHom.inv_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [One M] [One N] [InvOneClass P] (g : OneHom N P) (f : OneHom M N) :
g⁻¹.comp f = (g.comp f)⁻¹
source
theorem ZeroHom.neg_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Zero M] [Zero N] [NegZeroClass P] (g : ZeroHom N P) (f : ZeroHom M N) :
(-g).comp f = -g.comp f
source
instance OneHom.instDiv {M : Type u_2} {N : Type u_3} [One M] [DivisionMonoid N] :
Div (OneHom M N)

Given two one-preserving morphisms `f`, `g`, `f / g` is the one-preserving morphism sending `x` to `f x / g x`.

Equations

- OneHom.instDiv = { div := fun (f g : OneHom M N) => { toFun := fun (m : M) => f m / g m, map_one' := ⋯ } }

source
instance ZeroHom.instSub {M : Type u_2} {N : Type u_3} [Zero M] [SubtractionMonoid N] :
Sub (ZeroHom M N)

Given two zero-preserving morphisms `f`, `g`, `f - g` is the additive morphism sending `x` to `f x - g x`.

Equations

- ZeroHom.instSub = { sub := fun (f g : ZeroHom M N) => { toFun := fun (m : M) => f m - g m, map_zero' := ⋯ } }

source
theorem OneHom.coe_div {M : Type u_8} {N : Type u_9} [One M] [DivisionMonoid N] (f g : OneHom M N) :
⇑(f / g) = ⇑f / ⇑g
source
theorem ZeroHom.coe_sub {M : Type u_8} {N : Type u_9} [Zero M] [SubtractionMonoid N] (f g : ZeroHom M N) :
⇑(f - g) = ⇑f - ⇑g
source
@[simp]
theorem OneHom.div_apply {M : Type u_8} {N : Type u_9} [One M] [DivisionMonoid N] (f g : OneHom M N) (x : M) :
(f / g) x = f x / g x
source
@[simp]
theorem ZeroHom.sub_apply {M : Type u_8} {N : Type u_9} [Zero M] [SubtractionMonoid N] (f g : ZeroHom M N) (x : M) :
(f - g) x = f x - g x
source
theorem OneHom.div_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [One M] [One N] [DivisionMonoid P] (g₁ g₂ : OneHom N P) (f : OneHom M N) :
(g₁ / g₂).comp f = g₁.comp f / g₂.comp f
source
theorem ZeroHom.sub_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Zero M] [Zero N] [SubtractionMonoid P] (g₁ g₂ : ZeroHom N P) (f : ZeroHom M N) :
(g₁ - g₂).comp f = g₁.comp f - g₂.comp f
source
instance MulHom.instMul {M : Type u_2} {N : Type u_3} [Mul M] [CommSemigroup N] :
Mul (M →ₙ* N)

Given two mul morphisms `f`, `g` to a commutative semigroup, `f * g` is the mul morphism sending `x` to `f x * g x`.

Equations

- MulHom.instMul = { mul := fun (f g : M →ₙ* N) => { toFun := fun (m : M) => f m * g m, map_mul' := ⋯ } }

source
instance AddHom.instAdd {M : Type u_2} {N : Type u_3} [Add M] [AddCommSemigroup N] :
Add (M →ₙ+ N)

Given two additive morphisms `f`, `g` to an additive commutative semigroup, `f + g` is the additive morphism sending `x` to `f x + g x`.

Equations

- AddHom.instAdd = { add := fun (f g : M →ₙ+ N) => { toFun := fun (m : M) => f m + g m, map_add' := ⋯ } }

source
@[simp]
theorem MulHom.mul_apply {M : Type u_8} {N : Type u_9} [Mul M] [CommSemigroup N] (f g : M →ₙ* N) (x : M) :
(f * g) x = f x * g x
source
@[simp]
theorem AddHom.add_apply {M : Type u_8} {N : Type u_9} [Add M] [AddCommSemigroup N] (f g : M →ₙ+ N) (x : M) :
(f + g) x = f x + g x
source
theorem MulHom.mul_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Mul M] [Mul N] [CommSemigroup P] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
source
theorem AddHom.add_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Add M] [Add N] [AddCommSemigroup P] (g₁ g₂ : N →ₙ+ P) (f : M →ₙ+ N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
source
theorem MulHom.comp_mul {M : Type u_2} {N : Type u_3} {P : Type u_4} [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
source
theorem AddHom.comp_add {M : Type u_2} {N : Type u_3} {P : Type u_4} [Add M] [AddCommSemigroup N] [AddCommSemigroup P] (g : N →ₙ+ P) (f₁ f₂ : M →ₙ+ N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
source
theorem injective_iff_map_eq_one {F : Type u_7} {G : Type u_8} {H : Type u_9} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_one'`.

source
theorem injective_iff_map_eq_zero {F : Type u_7} {G : Type u_8} {H : Type u_9} [AddGroup G] [AddZeroClass H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_zero'`.

source
theorem injective_iff_map_eq_one' {F : Type u_7} {G : Type u_8} {H : Type u_9} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 ↔ a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see `injective_iff_map_eq_one`.

source
theorem injective_iff_map_eq_zero' {F : Type u_7} {G : Type u_8} {H : Type u_9} [AddGroup G] [AddZeroClass H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 ↔ a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see `injective_iff_map_eq_zero`.

source
def MonoidHom.ofMapMulInv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) :
G →* H

Makes a group homomorphism from a proof that the map preserves right division `fun x y => x * y⁻¹`. See also `MonoidHom.of_map_div` for a version using `fun x y => x / y`.

Equations

- MonoidHom.ofMapMulInv f map_div = MonoidHom.mk' f ⋯

Instances For

source
def AddMonoidHom.ofMapAddNeg {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (map_sub : ∀ (a b : G), f (a + -b) = f a + -f b) :
G →+ H

Makes an additive group homomorphism from a proof that the map preserves the operation `fun a b => a + -b`. See also `AddMonoidHom.ofMapSub` for a version using `fun a b => a - b`.

Equations

- AddMonoidHom.ofMapAddNeg f map_div = AddMonoidHom.mk' f ⋯

Instances For

source
@[simp]
theorem MonoidHom.coe_of_map_mul_inv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) :
⇑(ofMapMulInv f map_div) = f
source
@[simp]
theorem AddMonoidHom.coe_of_map_add_neg {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (map_sub : ∀ (a b : G), f (a + -b) = f a + -f b) :
⇑(ofMapAddNeg f map_sub) = f
source
def MonoidHom.ofMapDiv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
G →* H

Define a morphism of additive groups given a map which respects ratios.

Equations

- MonoidHom.ofMapDiv f hf = MonoidHom.ofMapMulInv f ⋯

Instances For

source
def AddMonoidHom.ofMapSub {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
G →+ H

Define a morphism of additive groups given a map which respects difference.

Equations

- AddMonoidHom.ofMapSub f hf = AddMonoidHom.ofMapAddNeg f ⋯

Instances For

source
@[simp]
theorem MonoidHom.coe_of_map_div {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
⇑(ofMapDiv f hf) = f
source
@[simp]
theorem AddMonoidHom.coe_of_map_sub {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
⇑(ofMapSub f hf) = f
source
instance MonoidHom.mul {M : Type u_2} {N : Type u_3} [MulOneClass M] [CommMonoid N] :
Mul (M →* N)

Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism sending `x` to `f x * g x`.

Equations

- MonoidHom.mul = { mul := fun (f g : M →* N) => { toFun := fun (m : M) => f m * g m, map_one' := ⋯, map_mul' := ⋯ } }

source
instance AddMonoidHom.add {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] :
Add (M →+ N)

Given two additive monoid morphisms `f`, `g` to an additive commutative monoid, `f + g` is the additive monoid morphism sending `x` to `f x + g x`.

Equations

- AddMonoidHom.add = { add := fun (f g : M →+ N) => { toFun := fun (m : M) => f m + g m, map_zero' := ⋯, map_add' := ⋯ } }

source
@[simp]
theorem MonoidHom.mul_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [CommMonoid N] (f g : M →* N) (x : M) :
(f * g) x = f x * g x
source
@[simp]
theorem AddMonoidHom.add_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] (f g : M →+ N) (x : M) :
(f + g) x = f x + g x
source
theorem MonoidHom.mul_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [MulOneClass M] [CommMonoid N] [MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
source
theorem AddMonoidHom.add_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddZeroClass M] [AddCommMonoid N] [AddZeroClass P] (g₁ g₂ : M →+ N) (f : P →+ M) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
source
theorem MonoidHom.comp_mul {M : Type u_2} {N : Type u_3} {P : Type u_4} [MulOneClass M] [CommMonoid N] [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
source
theorem AddMonoidHom.comp_add {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f₁ f₂ : M →+ N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
source
instance MonoidHom.instInv {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] :
Inv (M →* G)

If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending `x` to `(f x)⁻¹`.

Equations

- MonoidHom.instInv = { inv := fun (f : M →* G) => MonoidHom.mk' (fun (g : M) => (f g)⁻¹) ⋯ }

source
instance AddMonoidHom.instNeg {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] :
Neg (M →+ G)

If `f` is an additive monoid homomorphism to an additive commutative group, then `-f` is the homomorphism sending `x` to `-(f x)`.

Equations

- AddMonoidHom.instNeg = { neg := fun (f : M →+ G) => AddMonoidHom.mk' (fun (g : M) => -f g) ⋯ }

source
@[simp]
theorem MonoidHom.inv_apply {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] (f : M →* G) (x : M) :
f⁻¹ x = (f x)⁻¹
source
@[simp]
theorem AddMonoidHom.neg_apply {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) (x : M) :
(-f) x = -f x
source
@[simp]
theorem MonoidHom.inv_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [MulOneClass M] [MulOneClass N] [CommGroup G] (φ : N →* G) (ψ : M →* N) :
φ⁻¹.comp ψ = (φ.comp ψ)⁻¹
source
@[simp]
theorem AddMonoidHom.neg_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommGroup G] (φ : N →+ G) (ψ : M →+ N) :
(-φ).comp ψ = -φ.comp ψ
source
@[simp]
theorem MonoidHom.comp_inv {M : Type u_2} {G : Type u_5} {H : Type u_6} [MulOneClass M] [CommGroup G] [CommGroup H] (φ : G →* H) (ψ : M →* G) :
φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
source
@[simp]
theorem AddMonoidHom.comp_neg {M : Type u_2} {G : Type u_5} {H : Type u_6} [AddZeroClass M] [AddCommGroup G] [AddCommGroup H] (φ : G →+ H) (ψ : M →+ G) :
φ.comp (-ψ) = -φ.comp ψ
source
instance MonoidHom.instDiv {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] :
Div (M →* G)

If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism sending `x` to `(f x) / (g x)`.

Equations

- MonoidHom.instDiv = { div := fun (f g : M →* G) => MonoidHom.mk' (fun (x : M) => f x / g x) ⋯ }

source
instance AddMonoidHom.instSub {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] :
Sub (M →+ G)

If `f` and `g` are monoid homomorphisms to an additive commutative group, then `f - g` is the homomorphism sending `x` to `(f x) - (g x)`.

Equations

- AddMonoidHom.instSub = { sub := fun (f g : M →+ G) => AddMonoidHom.mk' (fun (x : M) => f x - g x) ⋯ }

source
@[simp]
theorem MonoidHom.div_apply {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] (f g : M →* G) (x : M) :
(f / g) x = f x / g x
source
@[simp]
theorem AddMonoidHom.sub_apply {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] (f g : M →+ G) (x : M) :
(f - g) x = f x - g x
source
@[simp]
theorem MonoidHom.div_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [MulOneClass M] [MulOneClass N] [CommGroup G] (f g : N →* G) (h : M →* N) :
(f / g).comp h = f.comp h / g.comp h
source
@[simp]
theorem AddMonoidHom.sub_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommGroup G] (f g : N →+ G) (h : M →+ N) :
(f - g).comp h = f.comp h - g.comp h
source
@[simp]
theorem MonoidHom.comp_div {M : Type u_2} {G : Type u_5} {H : Type u_6} [MulOneClass M] [CommGroup G] [CommGroup H] (f : G →* H) (g h : M →* G) :
f.comp (g / h) = f.comp g / f.comp h
source
@[simp]
theorem AddMonoidHom.comp_sub {M : Type u_2} {G : Type u_5} {H : Type u_6} [AddZeroClass M] [AddCommGroup G] [AddCommGroup H] (f : G →+ H) (g h : M →+ G) :
f.comp (g - h) = f.comp g - f.comp h
source
def MonoidHom.commGroupOfInjective {G : Type u_5} {H : Type u_6} [Group G] [CommGroup H] (f : G →* H) (hf : Function.Injective ⇑f) :
CommGroup G

If `H` is commutative and `G →* H` is injective, then `G` is commutative.

Equations

- f.commGroupOfInjective hf = { toGroup := inst✝¹, mul_comm := ⋯ }

Instances For

source
def MonoidHom.commGroupOfSurjective {G : Type u_5} {H : Type u_6} [CommGroup G] [Group H] (f : G →* H) (hf : Function.Surjective ⇑f) :
CommGroup H

If `G` is commutative and `G →* H` is surjective, then `H` is commutative.

Equations

- f.commGroupOfSurjective hf = { toGroup := inst✝, mul_comm := ⋯ }

Instances For