Documentation

Mathlib.Algebra.Hom.Group

Monoid and group homomorphisms #

This file defines the bundled structures for monoid and group homomorphisms. Namely, we define MonoidHom (resp., AddMonoidHom) to be bundled homomorphisms between multiplicative (resp., additive) monoids or groups.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

This file also defines the lesser-used (and notation-less) homomorphism types which are used as building blocks for other homomorphisms:

Notations #

→+→+: Bundled AddMonoid homs. Also use for AddGroup homs.
→*→*: Bundled Monoid homs. Also use for Group homs.
→*₀→*₀: Bundled MonoidWithZero homs. Also use for GroupWithZero homs.
→ₙ*→ₙ*: Bundled Semigroup homs.

Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no GroupHom -- the idea is that MonoidHom is used. The constructor for MonoidHom needs a proof of map_one as well as map_mul; a separate constructor MonoidHom.mk' will construct group homs (i.e. monoid homs between groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type MonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Historically this file also included definitions of unbundled homomorphism classes; they were deprecated and moved to Deprecated/Group.

Tags #

MonoidHom, AddMonoidHom

structure ZeroHom (M : Type u_1) (N : Type u_2) [inst : Zero M] [inst : Zero N] :

Type (maxu_1u_2)

The underlying function
toFun : M → N
The proposition that the function preserves 0
map_zero' : toFun 0 = 0

ZeroHom M N is the type of functions M → N→ N that preserve zero.

When possible, instead of parametrizing results over (f : ZeroHom M N), you should parametrize over (F : Type _) [ZeroHomClass F M N] (f : F).

When you extend this structure, make sure to also extend ZeroHomClass.

Instances For

class ZeroHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : Zero M] [inst : Zero N] extends FunLike :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves 0
map_zero : ∀ (f : F), ↑f 0 = 0

ZeroHomClass F M N states that F is a type of zero-preserving homomorphisms.

You should extend this typeclass when you extend ZeroHom.

Instances

theorem NeZero.of_map {F : Type u_3} {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst : Zero M] [inst : ZeroHomClass F R M] (f : F) {r : R} [neZero : NeZero (↑f r)] :

theorem NeZero.of_injective {F : Type u_3} {R : Type u_1} {M : Type u_2} [inst : Zero R] {r : R} [inst : NeZero r] [inst : Zero M] [inst : ZeroHomClass F R M] {f : F} (hf : Function.Injective ↑f) :

NeZero (↑f r)

structure AddHom (M : Type u_1) (N : Type u_2) [inst : Add M] [inst : Add N] :

Type (maxu_1u_2)

The underlying function
toFun : M → N
The proposition that the function preserves addition
map_add' : ∀ (x y : M), toFun (x + y) = toFun x + toFun y

AddHom M N is the type of functions M → N→ N that preserve addition.

When possible, instead of parametrizing results over (f : AddHom M N), you should parametrize over (F : Type _) [AddHomClass F M N] (f : F).

When you extend this structure, make sure to extend AddHomClass.

Instances For

class AddHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : Add M] [inst : Add N] extends FunLike :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves addition
map_add : ∀ (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y

AddHomClass F M N states that F is a type of addition-preserving homomorphisms. You should declare an instance of this typeclass when you extend AddHom.

Instances

structure AddMonoidHom (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] extends ZeroHom :

Type (maxu_1u_2)

The proposition that the function preserves addition
map_add' : ∀ (x y : M), ZeroHom.toFun toZeroHom (x + y) = ZeroHom.toFun toZeroHom x + ZeroHom.toFun toZeroHom y

M →+ N→+ N is the type of functions M → N→ N that preserve the AddZeroClass structure.

AddMonoidHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N)→+ N), you should parametrize over (F : Type _) [AddMonoidHomClass F M N] (f : F).

When you extend this structure, make sure to extend AddMonoidHomClass.

Instances For

def «term_→+_» :

Lean.TrailingParserDescr

M →+ N→+ N denotes the type of additive monoid homomorphisms from M to N.

Equations

«term_→+_» = Lean.ParserDescr.trailingNode `term_→+_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+ ") (Lean.ParserDescr.cat `term 25))

class AddMonoidHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : AddZeroClass M] [inst : AddZeroClass N] extends AddHomClass :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves 0
map_zero : ∀ (f : F), ↑f 0 = 0

AddMonoidHomClass F M N states that F is a type of AddZeroClass-preserving homomorphisms.

You should also extend this typeclass when you extend AddMonoidHom.

Instances

structure OneHom (M : Type u_1) (N : Type u_2) [inst : One M] [inst : One N] :

Type (maxu_1u_2)

The underlying function
toFun : M → N
The proposition that the function preserves 1
map_one' : toFun 1 = 1

OneHom M N is the type of functions M → N→ N that preserve one.

When possible, instead of parametrizing results over (f : OneHom M N), you should parametrize over (F : Type _) [OneHomClass F M N] (f : F).

When you extend this structure, make sure to also extend OneHomClass.

Instances For

class OneHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : One M] [inst : One N] extends FunLike :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves 1
map_one : ∀ (f : F), ↑f 1 = 1

OneHomClass F M N states that F is a type of one-preserving homomorphisms. You should extend this typeclass when you extend OneHom.

Instances

instance ZeroHom.zeroHomClass {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

ZeroHomClass (ZeroHom M N) M N

Equations

ZeroHom.zeroHomClass = ZeroHomClass.mk (_ : ∀ (self : ZeroHom M N), ZeroHom.toFun self 0 = 0)

def ZeroHom.zeroHomClass.proof_1 {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) (g : ZeroHom M N) (h : f.toFun = g.toFun) :

f = g

Equations

(_ : f = g) = (_ : f = g)

instance OneHom.oneHomClass {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

OneHomClass (OneHom M N) M N

Equations

OneHom.oneHomClass = OneHomClass.mk (_ : ∀ (self : OneHom M N), OneHom.toFun self 1 = 1)

@[simp]

theorem map_zero {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Zero M] [inst : Zero N] [inst : ZeroHomClass F M N] (f : F) :

↑f 0 = 0

@[simp]

theorem map_one {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : One M] [inst : One N] [inst : OneHomClass F M N] (f : F) :

↑f 1 = 1

theorem map_eq_zero_iff {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Zero M] [inst : Zero N] [inst : ZeroHomClass F M N] (f : F) (hf : Function.Injective ↑f) {x : M} :

↑f x = 0 ↔ x = 0

theorem map_eq_one_iff {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : One M] [inst : One N] [inst : OneHomClass F M N] (f : F) (hf : Function.Injective ↑f) {x : M} :

↑f x = 1 ↔ x = 1

theorem map_ne_zero_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Zero R] [inst : Zero S] [inst : ZeroHomClass F R S] (f : F) (hf : Function.Injective ↑f) {x : R} :

↑f x ≠ 0 ↔ x ≠ 0

theorem map_ne_one_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : One R] [inst : One S] [inst : OneHomClass F R S] (f : F) (hf : Function.Injective ↑f) {x : R} :

↑f x ≠ 1 ↔ x ≠ 1

theorem ne_zero_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Zero R] [inst : Zero S] [inst : ZeroHomClass F R S] {f : F} {x : R} (hx : ↑f x ≠ 0) :

x ≠ 0

theorem ne_one_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : One R] [inst : One S] [inst : OneHomClass F R S] {f : F} {x : R} (hx : ↑f x ≠ 1) :

x ≠ 1

def ZeroHomClass.toZeroHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Zero M] [inst : Zero N] [inst : ZeroHomClass F M N] (f : F) :

Turn an element of a type F satisfying ZeroHomClass F M N into an actual ZeroHom. This is declared as the default coercion from F to ZeroHom M N.

Equations

↑f = { toFun := ↑f, map_zero' := (_ : ↑f 0 = 0) }

def OneHomClass.toOneHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : One M] [inst : One N] [inst : OneHomClass F M N] (f : F) :

Turn an element of a type F satisfying OneHomClass F M N into an actual OneHom. This is declared as the default coercion from F to OneHom M N.

Equations

↑f = { toFun := ↑f, map_one' := (_ : ↑f 1 = 1) }

instance instCoeTCZeroHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Zero M] [inst : Zero N] [inst : ZeroHomClass F M N] :

CoeTC F (ZeroHom M N)

Any type satisfying ZeroHomClass can be cast into ZeroHom via ZeroHomClass.toZeroHom.

Equations

instCoeTCZeroHom = { coe := ZeroHomClass.toZeroHom }

instance instCoeTCOneHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : One M] [inst : One N] [inst : OneHomClass F M N] :

CoeTC F (OneHom M N)

Any type satisfying OneHomClass can be cast into OneHom via OneHomClass.toOneHom.

Equations

instCoeTCOneHom = { coe := OneHomClass.toOneHom }

@[simp]

theorem ZeroHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Zero M] [inst : Zero N] [inst : ZeroHomClass F M N] (f : F) :

↑↑f = ↑f

@[simp]

theorem OneHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : One M] [inst : One N] [inst : OneHomClass F M N] (f : F) :

↑↑f = ↑f

structure MulHom (M : Type u_1) (N : Type u_2) [inst : Mul M] [inst : Mul N] :

Type (maxu_1u_2)

The underlying function
toFun : M → N
The proposition that the function preserves multiplication
map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y

M →ₙ* N→ₙ* N is the type of functions M → N→ N that preserve multiplication. The ₙ in the notation stands for "non-unital" because it is intended to match the notation for NonUnitalAlgHom and NonUnitalRingHom, so a MulHom is a non-unital monoid hom.

When possible, instead of parametrizing results over (f : M →ₙ* N)→ₙ* N), you should parametrize over (F : Type _) [MulHomClass F M N] (f : F). When you extend this structure, make sure to extend MulHomClass.

Instances For

def «term_→ₙ*_» :

Lean.TrailingParserDescr

M →ₙ* N→ₙ* N denotes the type of multiplication-preserving maps from M to N.

Equations

«term_→ₙ*_» = Lean.ParserDescr.trailingNode `term_→ₙ*_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₙ* ") (Lean.ParserDescr.cat `term 25))

class MulHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : Mul M] [inst : Mul N] extends FunLike :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves multiplication
map_mul : ∀ (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y

MulHomClass F M N states that F is a type of multiplication-preserving homomorphisms.

You should declare an instance of this typeclass when you extend MulHom.

Instances

instance AddHom.addHomClass {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

AddHomClass (AddHom M N) M N

AddHom is a type of addition-preserving homomorphisms

Equations

AddHom.addHomClass = AddHomClass.mk (_ : ∀ (self : AddHom M N) (x y : M), AddHom.toFun self (x + y) = AddHom.toFun self x + AddHom.toFun self y)

def AddHom.addHomClass.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom M N) (h : f.toFun = g.toFun) :

f = g

Equations

(_ : f = g) = (_ : f = g)

instance MulHom.mulHomClass {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

MulHomClass (M →ₙ* N) M N

MulHom is a type of multiplication-preseving homomorphisms

Equations

MulHom.mulHomClass = MulHomClass.mk (_ : ∀ (self : M →ₙ* N) (x y : M), MulHom.toFun self (x * y) = MulHom.toFun self x * MulHom.toFun self y)

@[simp]

theorem map_add {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) (x : M) (y : M) :

↑f (x + y) = ↑f x + ↑f y

@[simp]

theorem map_mul {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) (x : M) (y : M) :

↑f (x * y) = ↑f x * ↑f y

def AddHomClass.toAddHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) :

Turn an element of a type F satisfying AddHomClass F M N into an actual AddHom. This is declared as the default coercion from F to M →ₙ+ N→ₙ+ N.

Equations

↑f = { toFun := ↑f, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) }

def MulHomClass.toMulHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) :

Turn an element of a type F satisfying MulHomClass F M N into an actual MulHom. This is declared as the default coercion from F to M →ₙ* N→ₙ* N.

Equations

↑f = { toFun := ↑f, map_mul' := (_ : ∀ (x y : M), ↑f (x * y) = ↑f x * ↑f y) }

instance instCoeTCAddHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] :

CoeTC F (AddHom M N)

Any type satisfying AddHomClass can be cast into AddHom via AddHomClass.toAddHom.

Equations

instCoeTCAddHom = { coe := AddHomClass.toAddHom }

instance instCoeTCMulHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] :

CoeTC F (M →ₙ* N)

Any type satisfying MulHomCLass can be cast into MulHom via MulHomClass.toMulHom.

Equations

instCoeTCMulHom = { coe := MulHomClass.toMulHom }

@[simp]

theorem AddHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) :

↑↑f = ↑f

@[simp]

theorem MulHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) :

↑↑f = ↑f

structure MonoidHom (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst : MulOneClass N] extends OneHom :

Type (maxu_1u_2)

The proposition that the function preserves multiplication
map_mul' : ∀ (x y : M), OneHom.toFun toOneHom (x * y) = OneHom.toFun toOneHom x * OneHom.toFun toOneHom y

M →* N→* N is the type of functions M → N→ N that preserve the Monoid structure. MonoidHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N)→+ N), you should parametrize over (F : Type _) [MonoidHomClass F M N] (f : F).

When you extend this structure, make sure to extend MonoidHomClass.

Instances For

def «term_→*_» :

Lean.TrailingParserDescr

M →* N→* N denotes the type of monoid homomorphisms from M to N.

Equations

«term_→*_» = Lean.ParserDescr.trailingNode `term_→*_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →* ") (Lean.ParserDescr.cat `term 25))

class MonoidHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : MulOneClass M] [inst : MulOneClass N] extends MulHomClass :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves 1
map_one : ∀ (f : F), ↑f 1 = 1

MonoidHomClass F M N states that F is a type of Monoid-preserving homomorphisms. You should also extend this typeclass when you extend MonoidHom.

Instances

def AddMonoidHom.addMonoidHomClass.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : M →+ N) (h : (fun f => (↑f).toFun) f = (fun f => (↑f).toFun) g) :

f = g

Equations

(_ : f = g) = (_ : f = g)

instance AddMonoidHom.addMonoidHomClass {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddMonoidHomClass (M →+ N) M N

Equations

AddMonoidHom.addMonoidHomClass = AddMonoidHomClass.mk (_ : ∀ (f : M →+ N), ZeroHom.toFun (↑f) 0 = 0)

def AddMonoidHom.addMonoidHomClass.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

ZeroHom.toFun (↑f) 0 = 0

Equations

(_ : ZeroHom.toFun (↑f) 0 = 0) = (_ : ZeroHom.toFun (↑f) 0 = 0)

instance MonoidHom.monoidHomClass {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

MonoidHomClass (M →* N) M N

Equations

MonoidHom.monoidHomClass = MonoidHomClass.mk (_ : ∀ (f : M →* N), OneHom.toFun (↑f) 1 = 1)

def AddMonoidHomClass.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} {F : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] (f : F) :

ZeroHom.toFun (↑f) 0 = 0

Equations

(_ : ZeroHom.toFun (↑f) 0 = 0) = (_ : ZeroHom.toFun (↑f) 0 = 0)

def AddMonoidHomClass.toAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} {F : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] (f : F) (x : M) (y : M) :

AddHom.toFun (↑f) (x + y) = AddHom.toFun (↑f) x + AddHom.toFun (↑f) y

Equations

(_ : ∀ (x y : M), AddHom.toFun (↑f) (x + y) = AddHom.toFun (↑f) x + AddHom.toFun (↑f) y) = (_ : ∀ (x y : M), AddHom.toFun (↑f) (x + y) = AddHom.toFun (↑f) x + AddHom.toFun (↑f) y)

def AddMonoidHomClass.toAddMonoidHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] (f : F) :

M →+ N

Turn an element of a type F satisfying AddMonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →+ N→+ N.

Equations

One or more equations did not get rendered due to their size.

def MonoidHomClass.toMonoidHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MonoidHomClass F M N] (f : F) :

M →* N

Turn an element of a type F satisfying MonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →* N→* N.

Equations

One or more equations did not get rendered due to their size.

instance instCoeTCAddMonoidHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] :

CoeTC F (M →+ N)

Any type satisfying AddMonoidHomClass can be cast into AddMonoidHom via AddMonoidHomClass.toAddMonoidHom.

Equations

instCoeTCAddMonoidHom = { coe := AddMonoidHomClass.toAddMonoidHom }

instance instCoeTCMonoidHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MonoidHomClass F M N] :

CoeTC F (M →* N)

Any type satisfying MonoidHomClass can be cast into MonoidHom via MonoidHomClass.toMonoidHom.

Equations

instCoeTCMonoidHom = { coe := MonoidHomClass.toMonoidHom }

@[simp]

theorem AddMonoidHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] (f : F) :

↑↑f = ↑f

@[simp]

theorem MonoidHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MonoidHomClass F M N] (f : F) :

↑↑f = ↑f

theorem map_add_eq_zero {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass F M N] (f : F) {a : M} {b : M} (h : a + b = 0) :

↑f a + ↑f b = 0

theorem map_mul_eq_one {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MonoidHomClass F M N] (f : F) {a : M} {b : M} (h : a * b = 1) :

↑f a * ↑f b = 1

theorem map_sub' {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : SubNegMonoid G] [inst : SubNegMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (hf : ∀ (a : G), ↑f (-a) = -↑f a) (a : G) (b : G) :

↑f (a - b) = ↑f a - ↑f b

theorem map_div' {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : DivInvMonoid G] [inst : DivInvMonoid H] [inst : MonoidHomClass F G H] (f : F) (hf : ∀ (a : G), ↑f a⁻¹ = (↑f a)⁻¹) (a : G) (b : G) :

↑f (a / b) = ↑f a / ↑f b

@[simp]

theorem map_neg {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (a : G) :

↑f (-a) = -↑f a

Additive group homomorphisms preserve negation.

@[simp]

theorem map_inv {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Group G] [inst : DivisionMonoid H] [inst : MonoidHomClass F G H] (f : F) (a : G) :

↑f a⁻¹ = (↑f a)⁻¹

Group homomorphisms preserve inverse.

theorem map_add_neg {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (a : G) (b : G) :

↑f (a + -b) = ↑f a + -↑f b

Additive group homomorphisms preserve subtraction.

theorem map_mul_inv {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Group G] [inst : DivisionMonoid H] [inst : MonoidHomClass F G H] (f : F) (a : G) (b : G) :

↑f (a * b⁻¹) = ↑f a * (↑f b)⁻¹

Group homomorphisms preserve division.

@[simp]

theorem map_sub {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (a : G) (b : G) :

↑f (a - b) = ↑f a - ↑f b

Additive group homomorphisms preserve subtraction.

@[simp]

theorem map_div {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Group G] [inst : DivisionMonoid H] [inst : MonoidHomClass F G H] (f : F) (a : G) (b : G) :

↑f (a / b) = ↑f a / ↑f b

Group homomorphisms preserve division.

abbrev map_nsmul.match_1 (motive : ℕ → Prop) :

(x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

map_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

@[simp]

theorem map_nsmul {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : AddMonoid G] [inst : AddMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (n : ℕ) (a : G) :

↑f (n • a) = n • ↑f a

@[simp]

theorem map_pow {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Monoid G] [inst : Monoid H] [inst : MonoidHomClass F G H] (f : F) (a : G) (n : ℕ) :

↑f (a ^ n) = ↑f a ^ n

theorem map_zsmul' {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : SubNegMonoid G] [inst : SubNegMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (hf : ∀ (x : G), ↑f (-x) = -↑f x) (a : G) (n : ℤ) :

↑f (n • a) = n • ↑f a

abbrev map_zsmul'.match_1 (motive : ℤ → Prop) :

(x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

Equations

map_zsmul'.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a

theorem map_zpow' {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : DivInvMonoid G] [inst : DivInvMonoid H] [inst : MonoidHomClass F G H] (f : F) (hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹) (a : G) (n : ℤ) :

↑f (a ^ n) = ↑f a ^ n

@[simp]

theorem map_zsmul {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass F G H] (f : F) (n : ℤ) (g : G) :

↑f (n • g) = n • ↑f g

Additive group homomorphisms preserve integer scaling.

@[simp]

theorem map_zpow {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Group G] [inst : DivisionMonoid H] [inst : MonoidHomClass F G H] (f : F) (g : G) (n : ℤ) :

↑f (g ^ n) = ↑f g ^ n

Group homomorphisms preserve integer power.

structure MonoidWithZeroHom (M : Type u_1) (N : Type u_2) [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] extends ZeroHom :

Type (maxu_1u_2)

The proposition that the function preserves 1
map_one' : ZeroHom.toFun toZeroHom 1 = 1
The proposition that the function preserves multiplication
map_mul' : ∀ (x y : M), ZeroHom.toFun toZeroHom (x * y) = ZeroHom.toFun toZeroHom x * ZeroHom.toFun toZeroHom y

M →*₀ N→*₀ N is the type of functions M → N→ N that preserve the MonoidWithZero structure.

MonoidWithZeroHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →*₀ N)→*₀ N), you should parametrize over (F : Type _) [MonoidWithZeroHomClass F M N] (f : F).

When you extend this structure, make sure to extend MonoidWithZeroHomClass.

Instances For

def «term_→*₀_» :

Lean.TrailingParserDescr

M →*₀ N→*₀ N denotes the type of zero-preserving monoid homomorphisms from M to N.

Equations

«term_→*₀_» = Lean.ParserDescr.trailingNode `term_→*₀_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →*₀ ") (Lean.ParserDescr.cat `term 25))

class MonoidWithZeroHomClass (F : Type u_1) (M : outParam (Type u_2)) (N : outParam (Type u_3)) [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] extends MonoidHomClass :

Type (max(maxu_1u_2)u_3)

The proposition that the function preserves 0
map_zero : ∀ (f : F), ↑f 0 = 0

MonoidWithZeroHomClass F M N states that F is a type of MonoidWithZero-preserving homomorphisms.

You should also extend this typeclass when you extend MonoidWithZeroHom.

Instances

instance MonoidWithZeroHom.monoidWithZeroHomClass {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] :

MonoidWithZeroHomClass (M →*₀ N) M N

Equations

MonoidWithZeroHom.monoidWithZeroHomClass = MonoidWithZeroHomClass.mk (_ : ∀ (f : M →*₀ N), ZeroHom.toFun (↑f) 0 = 0)

def MonoidWithZeroHomClass.toMonoidWithZeroHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MonoidWithZeroHomClass F M N] (f : F) :

Turn an element of a type F satisfying MonoidWithZeroHomClass F M N into an actual MonoidWithZeroHom. This is declared as the default coercion from F to M →*₀ N→*₀ N.

Equations

One or more equations did not get rendered due to their size.

instance instCoeTCMonoidWithZeroHom {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MonoidWithZeroHomClass F M N] :

CoeTC F (M →*₀ N)

Any type satisfying MonoidWithZeroHomClass can be cast into MonoidWithZeroHom via MonoidWithZeroHomClass.toMonoidWithZeroHom.

Equations

instCoeTCMonoidWithZeroHom = { coe := MonoidWithZeroHomClass.toMonoidWithZeroHom }

@[simp]

theorem MonoidWithZeroHom.coe_coe {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MonoidWithZeroHomClass F M N] (f : F) :

↑↑f = ↑f

Bundled morphisms can be down-cast to weaker bundlings

instance AddMonoidHom.coeToZeroHom {M : Type u_1} {N : Type u_2} :

{x : AddZeroClass M} → {x_1 : AddZeroClass N} → Coe (M →+ N) (ZeroHom M N)

AddMonoidHom down-cast to a ZeroHom, forgetting the additive property

Equations

AddMonoidHom.coeToZeroHom = { coe := AddMonoidHom.toZeroHom }

instance MonoidHom.coeToOneHom {M : Type u_1} {N : Type u_2} :

{x : MulOneClass M} → {x_1 : MulOneClass N} → Coe (M →* N) (OneHom M N)

MonoidHom down-cast to a OneHom, forgetting the multiplicative property.

Equations

MonoidHom.coeToOneHom = { coe := MonoidHom.toOneHom }

instance AddMonoidHom.coeToAddHom {M : Type u_1} {N : Type u_2} :

{x : AddZeroClass M} → {x_1 : AddZeroClass N} → Coe (M →+ N) (AddHom M N)

AddMonoidHom down-cast to an AddHom, forgetting the 0-preserving property.

Equations

AddMonoidHom.coeToAddHom = { coe := AddMonoidHom.toAddHom }

instance MonoidHom.coeToMulHom {M : Type u_1} {N : Type u_2} :

{x : MulOneClass M} → {x_1 : MulOneClass N} → Coe (M →* N) (M →ₙ* N)

MonoidHom down-cast to a MulHom, forgetting the 1-preserving property.

Equations

MonoidHom.coeToMulHom = { coe := MonoidHom.toMulHom }

instance MonoidWithZeroHom.coeToMonoidHom {M : Type u_1} {N : Type u_2} :

{x : MulZeroOneClass M} → {x_1 : MulZeroOneClass N} → Coe (M →*₀ N) (M →* N)

MonoidWithZeroHom down-cast to a MonoidHom, forgetting the 0-preserving property.

Equations

MonoidWithZeroHom.coeToMonoidHom = { coe := MonoidWithZeroHom.toMonoidHom }

instance MonoidWithZeroHom.coeToZeroHom {M : Type u_1} {N : Type u_2} :

{x : MulZeroOneClass M} → {x_1 : MulZeroOneClass N} → Coe (M →*₀ N) (ZeroHom M N)

MonoidWithZeroHom down-cast to a ZeroHom, forgetting the monoidal property.

Equations

MonoidWithZeroHom.coeToZeroHom = { coe := MonoidWithZeroHom.toZeroHom }

@[simp]

theorem ZeroHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : M → N) (h1 : f 0 = 0) :

↑{ toFun := f, map_zero' := h1 } = f

@[simp]

theorem OneHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : M → N) (h1 : f 1 = 1) :

↑{ toFun := f, map_one' := h1 } = f

@[simp]

theorem ZeroHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

f.toFun = ↑f

@[simp]

theorem OneHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

f.toFun = ↑f

@[simp]

theorem AddHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M → N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :

↑{ toFun := f, map_add' := hmul } = f

@[simp]

theorem MulHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M → N) (hmul : ∀ (x y : M), f (x * y) = f x * f y) :

↑{ toFun := f, map_mul' := hmul } = f

@[simp]

theorem AddHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

f.toFun = ↑f

@[simp]

theorem MulHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :

f.toFun = ↑f

@[simp]

theorem AddMonoidHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : ZeroHom M N) (hmul : ∀ (x y : M), ZeroHom.toFun f (x + y) = ZeroHom.toFun f x + ZeroHom.toFun f y) :

↑{ toZeroHom := f, map_add' := hmul } = ↑f

@[simp]

theorem MonoidHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : OneHom M N) (hmul : ∀ (x y : M), OneHom.toFun f (x * y) = OneHom.toFun f x * OneHom.toFun f y) :

↑{ toOneHom := f, map_mul' := hmul } = ↑f

@[simp]

theorem AddMonoidHom.toZeroHom_coe {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

↑↑f = ↑f

@[simp]

theorem MonoidHom.toOneHom_coe {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

↑↑f = ↑f

@[simp]

theorem AddMonoidHom.toAddHom_coe {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

(↑f).toFun = ↑f

@[simp]

theorem MonoidHom.toMulHom_coe {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

(↑f).toFun = ↑f

theorem AddMonoidHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

(↑f).toFun = ↑f

theorem MonoidHom.toFun_eq_coe {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

(↑f).toFun = ↑f

@[simp]

theorem MonoidWithZeroHom.coe_mk {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : ZeroHom M N) (h1 : ZeroHom.toFun f 1 = 1) (hmul : ∀ (x y : M), ZeroHom.toFun f (x * y) = ZeroHom.toFun f x * ZeroHom.toFun f y) :

↑{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = ↑f

@[simp]

theorem MonoidWithZeroHom.toZeroHom_coe {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

↑↑f = ↑f

theorem MonoidWithZeroHom.toMonoidHom_coe {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

(↑↑f).toFun = ↑f

theorem ZeroHom.ext {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] ⦃f : ZeroHom M N⦄ ⦃g : ZeroHom M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem OneHom.ext {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] ⦃f : OneHom M N⦄ ⦃g : OneHom M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem AddHom.ext {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] ⦃f : AddHom M N⦄ ⦃g : AddHom M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem MulHom.ext {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] ⦃f : M →ₙ* N⦄ ⦃g : M →ₙ* N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem AddMonoidHom.ext {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] ⦃f : M →+ N⦄ ⦃g : M →+ N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem MonoidHom.ext {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] ⦃f : M →* N⦄ ⦃g : M →* N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem MonoidWithZeroHom.ext {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] ⦃f : M →*₀ N⦄ ⦃g : M →*₀ N⦄ (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

theorem ZeroHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] {f : ZeroHom M N} {g : ZeroHom M N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem OneHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] {f : OneHom M N} {g : OneHom M N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem AddHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {g : AddHom M N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem MulHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {g : M →ₙ* N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem AddMonoidHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : M →+ N} {g : M →+ N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem MonoidHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {f : M →* N} {g : M →* N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem MonoidWithZeroHom.congr_fun {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] {f : M →*₀ N} {g : M →*₀ N} (h : f = g) (x : M) :

↑f x = ↑g x

Deprecated: use FunLike.congr_fun instead.

theorem ZeroHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem OneHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem AddHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem MulHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem AddMonoidHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem MonoidHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem MonoidWithZeroHom.congr_arg {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) {x : M} {y : M} (h : x = y) :

↑f x = ↑f y

Deprecated: use FunLike.congr_arg instead.

theorem ZeroHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] ⦃f : ZeroHom M N⦄ ⦃g : ZeroHom M N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem OneHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] ⦃f : OneHom M N⦄ ⦃g : OneHom M N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem AddHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] ⦃f : AddHom M N⦄ ⦃g : AddHom M N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem MulHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] ⦃f : M →ₙ* N⦄ ⦃g : M →ₙ* N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem AddMonoidHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] ⦃f : M →+ N⦄ ⦃g : M →+ N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem MonoidHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] ⦃f : M →* N⦄ ⦃g : M →* N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem MonoidWithZeroHom.coe_inj {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] ⦃f : M →*₀ N⦄ ⦃g : M →*₀ N⦄ (h : ↑f = ↑g) :

f = g

Deprecated: use FunLike.coe_injective instead.

theorem ZeroHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] {f : ZeroHom M N} {g : ZeroHom M N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem OneHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] {f : OneHom M N} {g : OneHom M N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem AddHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {g : AddHom M N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem MulHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {g : M →ₙ* N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem AddMonoidHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : M →+ N} {g : M →+ N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem MonoidHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {f : M →* N} {g : M →* N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

theorem MonoidWithZeroHom.ext_iff {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] {f : M →*₀ N} {g : M →*₀ N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

Deprecated: use FunLike.ext_iff instead.

@[simp]

theorem ZeroHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) (h1 : ↑f 0 = 0) :

{ toFun := ↑f, map_zero' := h1 } = f

@[simp]

theorem OneHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) (h1 : ↑f 1 = 1) :

{ toFun := ↑f, map_one' := h1 } = f

@[simp]

theorem AddHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (hmul : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) :

{ toFun := ↑f, map_add' := hmul } = f

@[simp]

theorem MulHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (hmul : ∀ (x y : M), ↑f (x * y) = ↑f x * ↑f y) :

{ toFun := ↑f, map_mul' := hmul } = f

@[simp]

theorem AddMonoidHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (hmul : ∀ (x y : M), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) :

{ toZeroHom := ↑f, map_add' := hmul } = f

@[simp]

theorem MonoidHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (hmul : ∀ (x y : M), OneHom.toFun (↑f) (x * y) = OneHom.toFun (↑f) x * OneHom.toFun (↑f) y) :

{ toOneHom := ↑f, map_mul' := hmul } = f

@[simp]

theorem MonoidWithZeroHom.mk_coe {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) (h1 : ZeroHom.toFun (↑f) 1 = 1) (hmul : ∀ (x y : M), ZeroHom.toFun (↑f) (x * y) = ZeroHom.toFun (↑f) x * ZeroHom.toFun (↑f) y) :

{ toZeroHom := ↑f, map_one' := h1, map_mul' := hmul } = f

def ZeroHom.copy {M : Type u_1} {N : Type u_2} :

{x : Zero M} → {x_1 : Zero N} → (f : ZeroHom M N) → (f' : M → N) → f' = ↑f → ZeroHom M N

Copy of a ZeroHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

ZeroHom.copy f f' h = { toFun := f', map_zero' := (_ : f' 0 = 0) }

def ZeroHom.copy.proof_1 {M : Type u_2} {N : Type u_1} :

∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : M → N), f' = ↑f → f' 0 = 0

Equations

(_ : f' 0 = 0) = (_ : f' 0 = 0)

def OneHom.copy {M : Type u_1} {N : Type u_2} :

{x : One M} → {x_1 : One N} → (f : OneHom M N) → (f' : M → N) → f' = ↑f → OneHom M N

Copy of a OneHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

OneHom.copy f f' h = { toFun := f', map_one' := (_ : f' 1 = 1) }

def AddHom.copy {M : Type u_1} {N : Type u_2} :

{x : Add M} → {x_1 : Add N} → (f : AddHom M N) → (f' : M → N) → f' = ↑f → AddHom M N

Copy of an AddHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

AddHom.copy f f' h = { toFun := f', map_add' := (_ : ∀ (x y : M), f' (x + y) = f' x + f' y) }

def AddHom.copy.proof_1 {M : Type u_2} {N : Type u_1} :

∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : M → N), f' = ↑f → ∀ (x_2 y : M), f' (x_2 + y) = f' x_2 + f' y

Equations

(_ : ∀ (x y : M), f' (x + y) = f' x + f' y) = (_ : ∀ (x y : M), f' (x + y) = f' x + f' y)

def MulHom.copy {M : Type u_1} {N : Type u_2} :

{x : Mul M} → {x_1 : Mul N} → (f : M →ₙ* N) → (f' : M → N) → f' = ↑f → M →ₙ* N

Copy of a MulHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

MulHom.copy f f' h = { toFun := f', map_mul' := (_ : ∀ (x y : M), f' (x * y) = f' x * f' y) }

def AddMonoidHom.copy.proof_2 {M : Type u_2} {N : Type u_1} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : M → N) (h : f' = ↑f) (x_2 y : M), AddHom.toFun (AddHom.copy (↑f) f' h) (x_2 + y) = AddHom.toFun (AddHom.copy (↑f) f' h) x_2 + AddHom.toFun (AddHom.copy (↑f) f' h) y

Equations

One or more equations did not get rendered due to their size.

def AddMonoidHom.copy.proof_1 {M : Type u_2} {N : Type u_1} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : M → N) (h : f' = ↑f), ZeroHom.toFun (ZeroHom.copy (↑f) f' h) 0 = 0

Equations

(_ : ZeroHom.toFun (ZeroHom.copy (↑f) f' h) 0 = 0) = (_ : ZeroHom.toFun (ZeroHom.copy (↑f) f' h) 0 = 0)

def AddMonoidHom.copy {M : Type u_1} {N : Type u_2} :

{x : AddZeroClass M} → {x_1 : AddZeroClass N} → (f : M →+ N) → (f' : M → N) → f' = ↑f → M →+ N

Copy of an AddMonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

One or more equations did not get rendered due to their size.

def MonoidHom.copy {M : Type u_1} {N : Type u_2} :

{x : MulOneClass M} → {x_1 : MulOneClass N} → (f : M →* N) → (f' : M → N) → f' = ↑f → M →* N

Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

One or more equations did not get rendered due to their size.

def MonoidWithZeroHom.copy {M : Type u_1} {N : Type u_2} :

{x : MulZeroOneClass M} → {x_1 : MulZeroOneClass N} → (f : M →*₀ N) → (f' : M → N) → f' = ↑f → M →* N

Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

One or more equations did not get rendered due to their size.

theorem ZeroHom.map_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

↑f 0 = 0

theorem OneHom.map_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

↑f 1 = 1

theorem AddMonoidHom.map_zero {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

↑f 0 = 0

If f is an additive monoid homomorphism then f 0 = 0.

theorem MonoidHom.map_one {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

↑f 1 = 1

If f is a monoid homomorphism then f 1 = 1.

theorem MonoidWithZeroHom.map_one {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

↑f 1 = 1

theorem MonoidWithZeroHom.map_zero {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

↑f 0 = 0

theorem AddHom.map_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (a : M) (b : M) :

↑f (a + b) = ↑f a + ↑f b

theorem MulHom.map_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (a : M) (b : M) :

↑f (a * b) = ↑f a * ↑f b

theorem AddMonoidHom.map_add {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (a : M) (b : M) :

↑f (a + b) = ↑f a + ↑f b

If f is an additive monoid homomorphism then f (a + b) = f a + f b.

theorem MonoidHom.map_mul {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (a : M) (b : M) :

↑f (a * b) = ↑f a * ↑f b

If f is a monoid homomorphism then f (a * b) = f a * f b.

theorem MonoidWithZeroHom.map_mul {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) (a : M) (b : M) :

↑f (a * b) = ↑f a * ↑f b

theorem AddMonoidHom.map_exists_right_neg {M : Type u_1} {N : Type u_2} {F : Type u_3} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddMonoidHomClass F M N] (f : F) {x_2 : M}, (∃ y, x_2 + y = 0) → ∃ y, ↑f x_2 + y = 0

Given an AddMonoid homomorphism f : M →+ N→+ N and an element x : M, if x has a right inverse, then f x has a right inverse too.

abbrev AddMonoidHom.map_exists_right_neg.match_1 {M : Type u_1} :

{x : AddZeroClass M} → {x_1 : M} → (motive : (∃ y, x_1 + y = 0) → Prop) → ∀ (hx : ∃ y, x_1 + y = 0), (∀ (y : M) (hy : x_1 + y = 0), motive (_ : ∃ y, x_1 + y = 0)) → motive hx

Equations

AddMonoidHom.map_exists_right_neg.match_1 motive hx h_1 = Exists.casesOn hx fun w h => h_1 w h

theorem MonoidHom.map_exists_right_inv {M : Type u_1} {N : Type u_2} {F : Type u_3} :

∀ {x : MulOneClass M} {x_1 : MulOneClass N} [inst : MonoidHomClass F M N] (f : F) {x_2 : M}, (∃ y, x_2 * y = 1) → ∃ y, ↑f x_2 * y = 1

Given a monoid homomorphism f : M →* N→* N and an element x : M, if x has a right inverse, then f x has a right inverse too. For elements invertible on both sides see IsUnit.map.

theorem AddMonoidHom.map_exists_left_neg {M : Type u_1} {N : Type u_2} {F : Type u_3} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddMonoidHomClass F M N] (f : F) {x_2 : M}, (∃ y, y + x_2 = 0) → ∃ y, y + ↑f x_2 = 0

Given an AddMonoid homomorphism f : M →+ N→+ N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsAddUnit.map.

abbrev AddMonoidHom.map_exists_left_neg.match_1 {M : Type u_1} :

{x : AddZeroClass M} → {x_1 : M} → (motive : (∃ y, y + x_1 = 0) → Prop) → ∀ (hx : ∃ y, y + x_1 = 0), (∀ (y : M) (hy : y + x_1 = 0), motive (_ : ∃ y, y + x_1 = 0)) → motive hx

Equations

AddMonoidHom.map_exists_left_neg.match_1 motive hx h_1 = Exists.casesOn hx fun w h => h_1 w h

theorem MonoidHom.map_exists_left_inv {M : Type u_1} {N : Type u_2} {F : Type u_3} :

∀ {x : MulOneClass M} {x_1 : MulOneClass N} [inst : MonoidHomClass F M N] (f : F) {x_2 : M}, (∃ y, y * x_2 = 1) → ∃ y, y * ↑f x_2 = 1

Given a monoid homomorphism f : M →* N→* N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsUnit.map.

def negAddMonoidHom {α : Type u_1} [inst : SubtractionCommMonoid α] :

α →+ α

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

Equations

negAddMonoidHom = { toZeroHom := { toFun := Neg.neg, map_zero' := (_ : -0 = 0) }, map_add' := (_ : ∀ (a b : α), -(a + b) = -a + -b) }

def negAddMonoidHom.proof_1 {α : Type u_1} [inst : SubtractionCommMonoid α] :

-0 = 0

Equations

(_ : -0 = 0) = (_ : -0 = 0)

def invMonoidHom {α : Type u_1} [inst : DivisionCommMonoid α] :

α →* α

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

Equations

invMonoidHom = { toOneHom := { toFun := Inv.inv, map_one' := (_ : 1⁻¹ = 1) }, map_mul' := (_ : ∀ (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹) }

@[simp]

theorem coe_invMonoidHom {α : Type u_1} [inst : DivisionCommMonoid α] :

↑invMonoidHom = Inv.inv

@[simp]

theorem invMonoidHom_apply {α : Type u_1} [inst : DivisionCommMonoid α] (a : α) :

↑invMonoidHom a = a⁻¹

def ZeroHom.id (M : Type u_1) [inst : Zero M] :

The identity map from an type with zero to itself.

Equations

ZeroHom.id M = { toFun := fun x => x, map_zero' := (_ : (fun x => x) 0 = (fun x => x) 0) }

def ZeroHom.id.proof_1 (M : Type u_1) [inst : Zero M] :

(fun x => x) 0 = (fun x => x) 0

Equations

(_ : (fun x => x) 0 = (fun x => x) 0) = (_ : (fun x => x) 0 = (fun x => x) 0)

@[simp]

theorem OneHom.id_apply (M : Type u_1) [inst : One M] (x : M) :

↑(OneHom.id M) x = x

@[simp]

theorem ZeroHom.id_apply (M : Type u_1) [inst : Zero M] (x : M) :

↑(ZeroHom.id M) x = x

def OneHom.id (M : Type u_1) [inst : One M] :

The identity map from a type with 1 to itself.

Equations

OneHom.id M = { toFun := fun x => x, map_one' := (_ : (fun x => x) 1 = (fun x => x) 1) }

def AddHom.id.proof_1 (M : Type u_1) [inst : Add M] :

∀ (x x_1 : M), (fun x => x) (x + x_1) = (fun x => x) (x + x_1)

Equations

(_ : (fun x => x) (x + x) = (fun x => x) (x + x)) = (_ : (fun x => x) (x + x) = (fun x => x) (x + x))

def AddHom.id (M : Type u_1) [inst : Add M] :

The identity map from an type with addition to itself.

Equations

AddHom.id M = { toFun := fun x => x, map_add' := (_ : ∀ (x x_1 : M), (fun x => x) (x + x_1) = (fun x => x) (x + x_1)) }

@[simp]

theorem MulHom.id_apply (M : Type u_1) [inst : Mul M] (x : M) :

↑(MulHom.id M) x = x

@[simp]

theorem AddHom.id_apply (M : Type u_1) [inst : Add M] (x : M) :

↑(AddHom.id M) x = x

def MulHom.id (M : Type u_1) [inst : Mul M] :

The identity map from a type with multiplication to itself.

Equations

MulHom.id M = { toFun := fun x => x, map_mul' := (_ : ∀ (x x_1 : M), (fun x => x) (x * x_1) = (fun x => x) (x * x_1)) }

def AddMonoidHom.id.proof_2 (M : Type u_1) [inst : AddZeroClass M] :

∀ (x x_1 : M), ZeroHom.toFun { toFun := fun x => x, map_zero' := (_ : (fun x => x) 0 = (fun x => x) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun x => x, map_zero' := (_ : (fun x => x) 0 = (fun x => x) 0) } (x + x_1)

Equations

One or more equations did not get rendered due to their size.

def AddMonoidHom.id (M : Type u_1) [inst : AddZeroClass M] :

M →+ M

The identity map from an additive monoid to itself.

Equations

One or more equations did not get rendered due to their size.

def AddMonoidHom.id.proof_1 (M : Type u_1) [inst : AddZeroClass M] :

(fun x => x) 0 = (fun x => x) 0

Equations

(_ : (fun x => x) 0 = (fun x => x) 0) = (_ : (fun x => x) 0 = (fun x => x) 0)

@[simp]

theorem AddMonoidHom.id_apply (M : Type u_1) [inst : AddZeroClass M] (x : M) :

↑(AddMonoidHom.id M) x = x

@[simp]

theorem MonoidHom.id_apply (M : Type u_1) [inst : MulOneClass M] (x : M) :

↑(MonoidHom.id M) x = x

def MonoidHom.id (M : Type u_1) [inst : MulOneClass M] :

M →* M

The identity map from a monoid to itself.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidWithZeroHom.id_apply (M : Type u_1) [inst : MulZeroOneClass M] (x : M) :

↑(MonoidWithZeroHom.id M) x = x

def MonoidWithZeroHom.id (M : Type u_1) [inst : MulZeroOneClass M] :

The identity map from a MonoidWithZero to itself.

Equations

One or more equations did not get rendered due to their size.

def ZeroHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :

Composition of ZeroHoms as a ZeroHom.

Equations

ZeroHom.comp hnp hmn = { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : ↑hnp (↑hmn 0) = 0) }

def ZeroHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Zero M] [inst : Zero N] [inst : Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :

↑hnp (↑hmn 0) = 0

Equations

(_ : ↑hnp (↑hmn 0) = 0) = (_ : ↑hnp (↑hmn 0) = 0)

def OneHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] (hnp : OneHom N P) (hmn : OneHom M N) :

Composition of OneHoms as a OneHom.

Equations

OneHom.comp hnp hmn = { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) }

def AddHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] (hnp : AddHom N P) (hmn : AddHom M N) (x : M) (y : M) :

↑hnp (↑hmn (x + y)) = ↑hnp (↑hmn x) + ↑hnp (↑hmn y)

Equations

(_ : ↑hnp (↑hmn (x + y)) = ↑hnp (↑hmn x) + ↑hnp (↑hmn y)) = (_ : ↑hnp (↑hmn (x + y)) = ↑hnp (↑hmn x) + ↑hnp (↑hmn y))

def AddHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (hnp : AddHom N P) (hmn : AddHom M N) :

Composition of AddHoms as a AddHom.

Equations

AddHom.comp hnp hmn = { toFun := ↑hnp ∘ ↑hmn, map_add' := (_ : ∀ (x y : M), ↑hnp (↑hmn (x + y)) = ↑hnp (↑hmn x) + ↑hnp (↑hmn y)) }

def MulHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) :

Composition of MulHoms as a MulHom.

Equations

MulHom.comp hnp hmn = { toFun := ↑hnp ∘ ↑hmn, map_mul' := (_ : ∀ (x y : M), ↑hnp (↑hmn (x * y)) = ↑hnp (↑hmn x) * ↑hnp (↑hmn y)) }

def AddMonoidHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) :

↑hnp (↑hmn 0) = 0

Equations

(_ : ↑hnp (↑hmn 0) = 0) = (_ : ↑hnp (↑hmn 0) = 0)

def AddMonoidHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) :

M →+ P

Composition of additive monoid morphisms as an additive monoid morphism.

Equations

One or more equations did not get rendered due to their size.

def AddMonoidHom.comp.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) (a : M) (a : M) :

↑hnp (↑hmn (a + a)) = ↑hnp (↑hmn a) + ↑hnp (↑hmn a)

Equations

(_ : ∀ (a a_1 : M), ↑hnp (↑hmn (a + a_1)) = ↑hnp (↑hmn a) + ↑hnp (↑hmn a_1)) = (_ : ∀ (a a_1 : M), ↑hnp (↑hmn (a + a_1)) = ↑hnp (↑hmn a) + ↑hnp (↑hmn a_1))

def MonoidHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (hnp : N →* P) (hmn : M →* N) :

M →* P

Composition of monoid morphisms as a monoid morphism.

Equations

MonoidHom.comp hnp hmn = { toOneHom := { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) }, map_mul' := (_ : ∀ (a a_1 : M), ↑hnp (↑hmn (a * a_1)) = ↑hnp (↑hmn a) * ↑hnp (↑hmn a_1)) }

def MonoidWithZeroHom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] (hnp : N →*₀ P) (hmn : M →*₀ N) :

Composition of MonoidWithZeroHoms as a MonoidWithZeroHom.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ZeroHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] (g : ZeroHom N P) (f : ZeroHom M N) :

↑(ZeroHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem OneHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] (g : OneHom N P) (f : OneHom M N) :

↑(OneHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem AddHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (g : AddHom N P) (f : AddHom M N) :

↑(AddHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem MulHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :

↑(MulHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem AddMonoidHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (g : N →+ P) (f : M →+ N) :

↑(AddMonoidHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem MonoidHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (g : N →* P) (f : M →* N) :

↑(MonoidHom.comp g f) = ↑g ∘ ↑f

@[simp]

theorem MonoidWithZeroHom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] (g : N →*₀ P) (f : M →*₀ N) :

↑(MonoidWithZeroHom.comp g f) = ↑g ∘ ↑f

theorem ZeroHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] (g : ZeroHom N P) (f : ZeroHom M N) (x : M) :

↑(ZeroHom.comp g f) x = ↑g (↑f x)

theorem OneHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] (g : OneHom N P) (f : OneHom M N) (x : M) :

↑(OneHom.comp g f) x = ↑g (↑f x)

theorem AddHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (g : AddHom N P) (f : AddHom M N) (x : M) :

↑(AddHom.comp g f) x = ↑g (↑f x)

theorem MulHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (g : N →ₙ* P) (f : M →ₙ* N) (x : M) :

↑(MulHom.comp g f) x = ↑g (↑f x)

theorem AddMonoidHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (g : N →+ P) (f : M →+ N) (x : M) :

↑(AddMonoidHom.comp g f) x = ↑g (↑f x)

theorem MonoidHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (g : N →* P) (f : M →* N) (x : M) :

↑(MonoidHom.comp g f) x = ↑g (↑f x)

theorem MonoidWithZeroHom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] (g : N →*₀ P) (f : M →*₀ N) (x : M) :

↑(MonoidWithZeroHom.comp g f) x = ↑g (↑f x)

theorem ZeroHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : Zero M] [inst : Zero N] [inst : Zero P] [inst : Zero Q] (f : ZeroHom M N) (g : ZeroHom N P) (h : ZeroHom P Q) :

ZeroHom.comp (ZeroHom.comp h g) f = ZeroHom.comp h (ZeroHom.comp g f)

Composition of additive monoid homomorphisms is associative.

theorem OneHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : One M] [inst : One N] [inst : One P] [inst : One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :

OneHom.comp (OneHom.comp h g) f = OneHom.comp h (OneHom.comp g f)

Composition of monoid homomorphisms is associative.

theorem AddHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] [inst : Add Q] (f : AddHom M N) (g : AddHom N P) (h : AddHom P Q) :

AddHom.comp (AddHom.comp h g) f = AddHom.comp h (AddHom.comp g f)

theorem MulHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : Mul M] [inst : Mul N] [inst : Mul P] [inst : Mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :

MulHom.comp (MulHom.comp h g) f = MulHom.comp h (MulHom.comp g f)

theorem AddMonoidHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] [inst : AddZeroClass Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q) :

AddMonoidHom.comp (AddMonoidHom.comp h g) f = AddMonoidHom.comp h (AddMonoidHom.comp g f)

theorem MonoidHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] [inst : MulOneClass Q] (f : M →* N) (g : N →* P) (h : P →* Q) :

MonoidHom.comp (MonoidHom.comp h g) f = MonoidHom.comp h (MonoidHom.comp g f)

theorem MonoidWithZeroHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_1} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] [inst : MulZeroOneClass Q] (f : M →*₀ N) (g : N →*₀ P) (h : P →*₀ Q) :

MonoidWithZeroHom.comp (MonoidWithZeroHom.comp h g) f = MonoidWithZeroHom.comp h (MonoidWithZeroHom.comp g f)

theorem ZeroHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] {g₁ : ZeroHom N P} {g₂ : ZeroHom N P} {f : ZeroHom M N} (hf : Function.Surjective ↑f) :

ZeroHom.comp g₁ f = ZeroHom.comp g₂ f ↔ g₁ = g₂

theorem OneHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] {g₁ : OneHom N P} {g₂ : OneHom N P} {f : OneHom M N} (hf : Function.Surjective ↑f) :

OneHom.comp g₁ f = OneHom.comp g₂ f ↔ g₁ = g₂

theorem AddHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] {g₁ : AddHom N P} {g₂ : AddHom N P} {f : AddHom M N} (hf : Function.Surjective ↑f) :

AddHom.comp g₁ f = AddHom.comp g₂ f ↔ g₁ = g₂

theorem MulHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] {g₁ : N →ₙ* P} {g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : Function.Surjective ↑f) :

MulHom.comp g₁ f = MulHom.comp g₂ f ↔ g₁ = g₂

theorem AddMonoidHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] {g₁ : N →+ P} {g₂ : N →+ P} {f : M →+ N} (hf : Function.Surjective ↑f) :

AddMonoidHom.comp g₁ f = AddMonoidHom.comp g₂ f ↔ g₁ = g₂

theorem MonoidHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] {g₁ : N →* P} {g₂ : N →* P} {f : M →* N} (hf : Function.Surjective ↑f) :

MonoidHom.comp g₁ f = MonoidHom.comp g₂ f ↔ g₁ = g₂

theorem MonoidWithZeroHom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] {g₁ : N →*₀ P} {g₂ : N →*₀ P} {f : M →*₀ N} (hf : Function.Surjective ↑f) :

MonoidWithZeroHom.comp g₁ f = MonoidWithZeroHom.comp g₂ f ↔ g₁ = g₂

theorem ZeroHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] {g : ZeroHom N P} {f₁ : ZeroHom M N} {f₂ : ZeroHom M N} (hg : Function.Injective ↑g) :

ZeroHom.comp g f₁ = ZeroHom.comp g f₂ ↔ f₁ = f₂

theorem OneHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] {g : OneHom N P} {f₁ : OneHom M N} {f₂ : OneHom M N} (hg : Function.Injective ↑g) :

OneHom.comp g f₁ = OneHom.comp g f₂ ↔ f₁ = f₂

theorem AddHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] {g : AddHom N P} {f₁ : AddHom M N} {f₂ : AddHom M N} (hg : Function.Injective ↑g) :

AddHom.comp g f₁ = AddHom.comp g f₂ ↔ f₁ = f₂

theorem MulHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] {g : N →ₙ* P} {f₁ : M →ₙ* N} {f₂ : M →ₙ* N} (hg : Function.Injective ↑g) :

MulHom.comp g f₁ = MulHom.comp g f₂ ↔ f₁ = f₂

theorem AddMonoidHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] {g : N →+ P} {f₁ : M →+ N} {f₂ : M →+ N} (hg : Function.Injective ↑g) :

AddMonoidHom.comp g f₁ = AddMonoidHom.comp g f₂ ↔ f₁ = f₂

theorem MonoidHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] {g : N →* P} {f₁ : M →* N} {f₂ : M →* N} (hg : Function.Injective ↑g) :

MonoidHom.comp g f₁ = MonoidHom.comp g f₂ ↔ f₁ = f₂

theorem MonoidWithZeroHom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] [inst : MulZeroOneClass P] {g : N →*₀ P} {f₁ : M →*₀ N} {f₂ : M →*₀ N} (hg : Function.Injective ↑g) :

MonoidWithZeroHom.comp g f₁ = MonoidWithZeroHom.comp g f₂ ↔ f₁ = f₂

theorem AddMonoidHom.toZeroHom_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

Function.Injective AddMonoidHom.toZeroHom

theorem MonoidHom.toOneHom_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Function.Injective MonoidHom.toOneHom

theorem AddMonoidHom.toAddHom_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

Function.Injective AddMonoidHom.toAddHom

theorem MonoidHom.toMulHom_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Function.Injective MonoidHom.toMulHom

theorem MonoidWithZeroHom.toMonoidHom_injective {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] :

Function.Injective MonoidWithZeroHom.toMonoidHom

theorem MonoidWithZeroHom.toZeroHom_injective {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] :

Function.Injective MonoidWithZeroHom.toZeroHom

@[simp]

theorem ZeroHom.comp_id {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

ZeroHom.comp f (ZeroHom.id M) = f

@[simp]

theorem OneHom.comp_id {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

OneHom.comp f (OneHom.id M) = f

@[simp]

theorem AddHom.comp_id {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

AddHom.comp f (AddHom.id M) = f

@[simp]

theorem MulHom.comp_id {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :

MulHom.comp f (MulHom.id M) = f

@[simp]

theorem AddMonoidHom.comp_id {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

AddMonoidHom.comp f (AddMonoidHom.id M) = f

@[simp]

theorem MonoidHom.comp_id {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

MonoidHom.comp f (MonoidHom.id M) = f

@[simp]

theorem MonoidWithZeroHom.comp_id {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

MonoidWithZeroHom.comp f (MonoidWithZeroHom.id M) = f

@[simp]

theorem ZeroHom.id_comp {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

ZeroHom.comp (ZeroHom.id N) f = f

@[simp]

theorem OneHom.id_comp {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

OneHom.comp (OneHom.id N) f = f

@[simp]

theorem AddHom.id_comp {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

AddHom.comp (AddHom.id N) f = f

@[simp]

theorem MulHom.id_comp {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :

MulHom.comp (MulHom.id N) f = f

@[simp]

theorem AddMonoidHom.id_comp {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

AddMonoidHom.comp (AddMonoidHom.id N) f = f

@[simp]

theorem MonoidHom.id_comp {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

MonoidHom.comp (MonoidHom.id N) f = f

@[simp]

theorem MonoidWithZeroHom.id_comp {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] (f : M →*₀ N) :

MonoidWithZeroHom.comp (MonoidWithZeroHom.id N) f = f

theorem AddMonoidHom.map_nsmul {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (a : M) (n : ℕ) :

↑f (n • a) = n • ↑f a

theorem MonoidHom.map_pow {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (a : M) (n : ℕ) :

↑f (a ^ n) = ↑f a ^ n

theorem AddMonoidHom.map_zsmul' {M : Type u_1} {N : Type u_2} [inst : SubNegMonoid M] [inst : SubNegMonoid N] (f : M →+ N) (hf : ∀ (x : M), ↑f (-x) = -↑f x) (a : M) (n : ℤ) :

↑f (n • a) = n • ↑f a

theorem MonoidHom.map_zpow' {M : Type u_1} {N : Type u_2} [inst : DivInvMonoid M] [inst : DivInvMonoid N] (f : M →* N) (hf : ∀ (x : M), ↑f x⁻¹ = (↑f x)⁻¹) (a : M) (n : ℤ) :

↑f (a ^ n) = ↑f a ^ n

def Monoid.End (M : Type u_1) [inst : MulOneClass M] :

Type u_1

The monoid of endomorphisms.

Equations

Monoid.End M = (M →* M)

instance Monoid.End.instMonoidEnd (M : Type u_1) [inst : MulOneClass M] :

Monoid (Monoid.End M)

Equations

Monoid.End.instMonoidEnd M = Monoid.mk (_ : ∀ (f : M →* M), MonoidHom.comp (MonoidHom.id M) f = f) (_ : ∀ (f : M →* M), MonoidHom.comp f (MonoidHom.id M) = f) npowRec

instance Monoid.End.instInhabitedEnd (M : Type u_1) [inst : MulOneClass M] :

Inhabited (Monoid.End M)

Equations

Monoid.End.instInhabitedEnd M = { default := 1 }

instance Monoid.End.instMonoidHomClassEnd (M : Type u_1) [inst : MulOneClass M] :

MonoidHomClass (Monoid.End M) M M

Equations

Monoid.End.instMonoidHomClassEnd M = MonoidHom.monoidHomClass

@[simp]

theorem Monoid.coe_one (M : Type u_1) [inst : MulOneClass M] :

↑1 = id

@[simp]

theorem Monoid.coe_mul (M : Type u_1) [inst : MulOneClass M] (f : Monoid.End M) (g : Monoid.End M) :

↑(f * g) = ↑f ∘ ↑g

def AddMonoid.End (A : Type u_1) [inst : AddZeroClass A] :

Type u_1

The monoid of endomorphisms.

Equations

AddMonoid.End A = (A →+ A)

instance AddMonoid.End.monoid (A : Type u_1) [inst : AddZeroClass A] :

Monoid (AddMonoid.End A)

Equations

AddMonoid.End.monoid A = Monoid.mk (_ : ∀ (f : A →+ A), AddMonoidHom.comp (AddMonoidHom.id A) f = f) (_ : ∀ (f : A →+ A), AddMonoidHom.comp f (AddMonoidHom.id A) = f) npowRec

instance AddMonoid.End.instInhabitedEnd (A : Type u_1) [inst : AddZeroClass A] :

Inhabited (AddMonoid.End A)

Equations

AddMonoid.End.instInhabitedEnd A = { default := 1 }

instance AddMonoid.End.instAddMonoidHomClassEnd (A : Type u_1) [inst : AddZeroClass A] :

AddMonoidHomClass (AddMonoid.End A) A A

Equations

AddMonoid.End.instAddMonoidHomClassEnd A = AddMonoidHom.addMonoidHomClass

@[simp]

theorem AddMonoid.coe_one (A : Type u_1) [inst : AddZeroClass A] :

↑1 = id

@[simp]

theorem AddMonoid.coe_mul (A : Type u_1) [inst : AddZeroClass A] (f : AddMonoid.End A) (g : AddMonoid.End A) :

↑(f * g) = ↑f ∘ ↑g

def instZeroZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] :

(fun x => 0) 0 = (fun x => 0) 0

Equations

(_ : (fun x => 0) 0 = (fun x => 0) 0) = (_ : (fun x => 0) 0 = (fun x => 0) 0)

instance instZeroZeroHom {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

Zero (ZeroHom M N)

0 is the homomorphism sending all elements to 0.

Equations

instZeroZeroHom = { zero := { toFun := fun x => 0, map_zero' := (_ : (fun x => 0) 0 = (fun x => 0) 0) } }

instance instOneOneHom {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

One (OneHom M N)

1 is the homomorphism sending all elements to 1.

Equations

instOneOneHom = { one := { toFun := fun x => 1, map_one' := (_ : (fun x => 1) 1 = (fun x => 1) 1) } }

def instZeroAddHomToAdd.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass N] :

M → M → 0 = 0 + 0

Equations

(_ : 0 = 0 + 0) = (_ : 0 = 0 + 0)

instance instZeroAddHomToAdd {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : AddZeroClass N] :

Zero (AddHom M N)

0 is the additive homomorphism sending all elements to 0.

Equations

instZeroAddHomToAdd = { zero := { toFun := fun x => 0, map_add' := (_ : M → M → 0 = 0 + 0) } }

instance instOneMulHomToMul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : MulOneClass N] :

One (M →ₙ* N)

1 is the multiplicative homomorphism sending all elements to 1.

Equations

instOneMulHomToMul = { one := { toFun := fun x => 1, map_mul' := (_ : M → M → 1 = 1 * 1) } }

instance instZeroAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

Zero (M →+ N)

0 is the additive monoid homomorphism sending all elements to 0.

Equations

instZeroAddMonoidHom = { zero := { toZeroHom := { toFun := fun x => 0, map_zero' := (_ : (fun x => 0) 0 = (fun x => 0) 0) }, map_add' := (_ : M → M → 0 = 0 + 0) } }

def instZeroAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass N] :

M → M → 0 = 0 + 0

Equations

(_ : 0 = 0 + 0) = (_ : 0 = 0 + 0)

def instZeroAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] :

(fun x => 0) 0 = (fun x => 0) 0

Equations

(_ : (fun x => 0) 0 = (fun x => 0) 0) = (_ : (fun x => 0) 0 = (fun x => 0) 0)

instance instOneMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

One (M →* N)

1 is the monoid homomorphism sending all elements to 1.

Equations

instOneMonoidHom = { one := { toOneHom := { toFun := fun x => 1, map_one' := (_ : (fun x => 1) 1 = (fun x => 1) 1) }, map_mul' := (_ : M → M → 1 = 1 * 1) } }

@[simp]

theorem ZeroHom.zero_apply {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (x : M) :

↑0 x = 0

@[simp]

theorem OneHom.one_apply {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (x : M) :

↑1 x = 1

@[simp]

theorem AddMonoidHom.zero_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (x : M) :

↑0 x = 0

@[simp]

theorem MonoidHom.one_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (x : M) :

↑1 x = 1

@[simp]

theorem ZeroHom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] (f : ZeroHom M N) :

ZeroHom.comp 0 f = 0

@[simp]

theorem OneHom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] (f : OneHom M N) :

OneHom.comp 1 f = 1

@[simp]

theorem ZeroHom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Zero M] [inst : Zero N] [inst : Zero P] (f : ZeroHom N P) :

ZeroHom.comp f 0 = 0

@[simp]

theorem OneHom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : One M] [inst : One N] [inst : One P] (f : OneHom N P) :

OneHom.comp f 1 = 1

instance instInhabitedZeroHom {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

Inhabited (ZeroHom M N)

Equations

instInhabitedZeroHom = { default := 0 }

instance instInhabitedOneHom {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

Inhabited (OneHom M N)

Equations

instInhabitedOneHom = { default := 1 }

instance instInhabitedAddHomToAdd {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : AddZeroClass N] :

Inhabited (AddHom M N)

Equations

instInhabitedAddHomToAdd = { default := 0 }

instance instInhabitedMulHomToMul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : MulOneClass N] :

Inhabited (M →ₙ* N)

Equations

instInhabitedMulHomToMul = { default := 1 }

instance instInhabitedAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

Inhabited (M →+ N)

Equations

instInhabitedAddMonoidHom = { default := 0 }

instance instInhabitedMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Inhabited (M →* N)

Equations

instInhabitedMonoidHom = { default := 1 }

instance instInhabitedMonoidWithZeroHom {M : Type u_1} [inst : MulZeroOneClass M] :

Inhabited (M →*₀ M)

Equations

instInhabitedMonoidWithZeroHom = { default := MonoidWithZeroHom.id M }

instance AddHom.instAddAddHomToAddToAddSemigroup {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : AddCommSemigroup N] :

Add (AddHom 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

One or more equations did not get rendered due to their size.

def AddHom.instAddAddHomToAddToAddSemigroup.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : AddCommSemigroup N] (f : AddHom M N) (g : AddHom M N) (x : M) (y : M) :

↑f (x + y) + ↑g (x + y) = ↑f x + ↑g x + (↑f y + ↑g y)

Equations

(_ : ↑f (x + y) + ↑g (x + y) = ↑f x + ↑g x + (↑f y + ↑g y)) = (_ : ↑f (x + y) + ↑g (x + y) = ↑f x + ↑g x + (↑f y + ↑g y))

instance MulHom.instMulMulHomToMulToSemigroup {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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

One or more equations did not get rendered due to their size.

@[simp]

theorem AddHom.add_apply {M : Type u_1} {N : Type u_2} :

∀ {x : Add M} {x_1 : AddCommSemigroup N} (f g : AddHom M N) (x_2 : M), ↑(f + g) x_2 = ↑f x_2 + ↑g x_2

@[simp]

theorem MulHom.mul_apply {M : Type u_1} {N : Type u_2} :

∀ {x : Mul M} {x_1 : CommSemigroup N} (f g : M →ₙ* N) (x_2 : M), ↑(f * g) x_2 = ↑f x_2 * ↑g x_2

theorem AddHom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : AddCommSemigroup P] (g₁ : AddHom N P) (g₂ : AddHom N P) (f : AddHom M N) :

AddHom.comp (g₁ + g₂) f = AddHom.comp g₁ f + AddHom.comp g₂ f

theorem MulHom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : CommSemigroup P] (g₁ : N →ₙ* P) (g₂ : N →ₙ* P) (f : M →ₙ* N) :

MulHom.comp (g₁ * g₂) f = MulHom.comp g₁ f * MulHom.comp g₂ f

theorem AddHom.comp_add {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : AddCommSemigroup N] [inst : AddCommSemigroup P] (g : AddHom N P) (f₁ : AddHom M N) (f₂ : AddHom M N) :

AddHom.comp g (f₁ + f₂) = AddHom.comp g f₁ + AddHom.comp g f₂

theorem MulHom.comp_mul {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : CommSemigroup N] [inst : CommSemigroup P] (g : N →ₙ* P) (f₁ : M →ₙ* N) (f₂ : M →ₙ* N) :

MulHom.comp g (f₁ * f₂) = MulHom.comp g f₁ * MulHom.comp g f₂

instance AddMonoidHom.add {M : Type u_1} {N : Type u_2} :

{x : AddZeroClass M} → [inst : 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

One or more equations did not get rendered due to their size.

def AddMonoidHom.add.proof_1 {M : Type u_2} {N : Type u_1} :

∀ {x : AddZeroClass M} [inst : AddCommMonoid N] (f g : M →+ N), ↑f 0 + ↑g 0 = 0

Equations

(_ : ↑f 0 + ↑g 0 = 0) = (_ : ↑f 0 + ↑g 0 = 0)

def AddMonoidHom.add.proof_2 {M : Type u_2} {N : Type u_1} :

∀ {x : AddZeroClass M} [inst : AddCommMonoid N] (f g : M →+ N) (x_1 y : M), ↑f (x_1 + y) + ↑g (x_1 + y) = ↑f x_1 + ↑g x_1 + (↑f y + ↑g y)

Equations

(_ : ↑f (x + y) + ↑g (x + y) = ↑f x + ↑g x + (↑f y + ↑g y)) = (_ : ↑f (x + y) + ↑g (x + y) = ↑f x + ↑g x + (↑f y + ↑g y))

instance MonoidHom.mul {M : Type u_1} {N : Type u_2} :

{x : MulOneClass M} → [inst : 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

One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.add_apply {M : Type u_1} {N : Type u_2} :

∀ {x : AddZeroClass M} {x_1 : AddCommMonoid N} (f g : M →+ N) (x_2 : M), ↑(f + g) x_2 = ↑f x_2 + ↑g x_2

@[simp]

theorem MonoidHom.mul_apply {M : Type u_1} {N : Type u_2} :

∀ {x : MulOneClass M} {x_1 : CommMonoid N} (f g : M →* N) (x_2 : M), ↑(f * g) x_2 = ↑f x_2 * ↑g x_2

@[simp]

theorem AddMonoidHom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) :

AddMonoidHom.comp 0 f = 0

@[simp]

theorem MonoidHom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) :

MonoidHom.comp 1 f = 1

@[simp]

theorem AddMonoidHom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : N →+ P) :

AddMonoidHom.comp f 0 = 0

@[simp]

theorem MonoidHom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : N →* P) :

MonoidHom.comp f 1 = 1

theorem AddMonoidHom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] (g₁ : N →+ P) (g₂ : N →+ P) (f : M →+ N) :

AddMonoidHom.comp (g₁ + g₂) f = AddMonoidHom.comp g₁ f + AddMonoidHom.comp g₂ f

theorem MonoidHom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] (g₁ : N →* P) (g₂ : N →* P) (f : M →* N) :

MonoidHom.comp (g₁ * g₂) f = MonoidHom.comp g₁ f * MonoidHom.comp g₂ f

theorem AddMonoidHom.comp_add {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddCommMonoid N] [inst : AddCommMonoid P] (g : N →+ P) (f₁ : M →+ N) (f₂ : M →+ N) :

AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂

theorem MonoidHom.comp_mul {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : CommMonoid N] [inst : CommMonoid P] (g : N →* P) (f₁ : M →* N) (f₂ : M →* N) :

MonoidHom.comp g (f₁ * f₂) = MonoidHom.comp g f₁ * MonoidHom.comp g f₂

theorem AddMonoidHom.map_neg {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] (f : α →+ β) (a : α) :

↑f (-a) = -↑f a

Additive group homomorphisms preserve negation.

theorem MonoidHom.map_inv {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] (f : α →* β) (a : α) :

↑f a⁻¹ = (↑f a)⁻¹

Group homomorphisms preserve inverse.

theorem AddMonoidHom.map_zsmul {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] (f : α →+ β) (g : α) (n : ℤ) :

↑f (n • g) = n • ↑f g

Additive group homomorphisms preserve integer scaling.

theorem MonoidHom.map_zpow {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ) :

↑f (g ^ n) = ↑f g ^ n

Group homomorphisms preserve integer power.

theorem AddMonoidHom.map_sub {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] (f : α →+ β) (g : α) (h : α) :

↑f (g - h) = ↑f g - ↑f h

Additive group homomorphisms preserve subtraction.

theorem MonoidHom.map_div {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] (f : α →* β) (g : α) (h : α) :

↑f (g / h) = ↑f g / ↑f h

Group homomorphisms preserve division.

theorem AddMonoidHom.map_add_neg {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : SubtractionMonoid β] (f : α →+ β) (g : α) (h : α) :

↑f (g + -h) = ↑f g + -↑f h

Additive group homomorphisms preserve subtraction.

theorem MonoidHom.map_mul_inv {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : DivisionMonoid β] (f : α →* β) (g : α) (h : α) :

↑f (g * h⁻¹) = ↑f g * (↑f h)⁻¹

Group homomorphisms preserve division.

theorem injective_iff_map_eq_zero {F : Type u_3} {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : AddZeroClass H] [inst : 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'.

theorem injective_iff_map_eq_one {F : Type u_3} {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : MulOneClass H] [inst : 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'.

theorem injective_iff_map_eq_zero' {F : Type u_3} {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : AddZeroClass H] [inst : 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.

theorem injective_iff_map_eq_one' {F : Type u_3} {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : MulOneClass H] [inst : 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.

def AddMonoidHom.mk'.proof_1 {M : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst : AddZeroClass M] (f : M → G) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :

f 0 = 0

Equations

(_ : f 0 = 0) = (_ : f 0 = 0)

def AddMonoidHom.mk' {M : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst : AddZeroClass M] (f : M → G) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :

M →+ G

Makes an additive group homomorphism from a proof that the map preserves addition.

Equations

AddMonoidHom.mk' f map_mul = { toZeroHom := { toFun := f, map_zero' := (_ : f 0 = 0) }, map_add' := map_mul }

@[simp]

theorem MonoidHom.mk'_apply {M : Type u_1} {G : Type u_2} [inst : Group G] [inst : MulOneClass M] (f : M → G) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :

↑(MonoidHom.mk' f map_mul) = f

@[simp]

theorem AddMonoidHom.mk'_apply {M : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst : AddZeroClass M] (f : M → G) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :

↑(AddMonoidHom.mk' f map_mul) = f

def MonoidHom.mk' {M : Type u_1} {G : Type u_2} [inst : Group G] [inst : MulOneClass M] (f : M → G) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :

M →* G

Makes a group homomorphism from a proof that the map preserves multiplication.

Equations

MonoidHom.mk' f map_mul = { toOneHom := { toFun := f, map_one' := (_ : f 1 = 1) }, map_mul' := map_mul }

def AddMonoidHom.ofMapAddNeg {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst : AddGroup H] (f : G → H) (map_div : ∀ (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 (_ : ∀ (x y : G), f (x + y) = f x + f y)

def AddMonoidHom.ofMapAddNeg.proof_1 {G : Type u_2} [inst : AddGroup G] {H : Type u_1} [inst : AddGroup H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) (x : G) (y : G) :

f (x + y) = f x + f y

Equations

(_ : f (x + y) = f x + f y) = (_ : f (x + y) = f x + f y)

def MonoidHom.ofMapMulInv {G : Type u_1} [inst : Group G] {H : Type u_2} [inst : 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 (_ : ∀ (x y : G), f (x * y) = f x * f y)

@[simp]

theorem AddMonoidHom.coe_of_map_add_neg {G : Type u_2} [inst : AddGroup G] {H : Type u_1} [inst : AddGroup H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) :

↑(AddMonoidHom.ofMapAddNeg f map_div) = f

@[simp]

theorem MonoidHom.coe_of_map_mul_inv {G : Type u_2} [inst : Group G] {H : Type u_1} [inst : Group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) :

↑(MonoidHom.ofMapMulInv f map_div) = f

def AddMonoidHom.ofMapSub.proof_1 {G : Type u_2} [inst : AddGroup G] {H : Type u_1} [inst : AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) (a : G) (a : G) :

f (a + -a) = f a + -f a

Equations

(_ : ∀ (a a_1 : G), f (a + -a_1) = f a + -f a_1) = (_ : ∀ (a a_1 : G), f (a + -a_1) = f a + -f a_1)

def AddMonoidHom.ofMapSub {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst : 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 (_ : ∀ (a a_1 : G), f (a + -a_1) = f a + -f a_1)

def MonoidHom.ofMapDiv {G : Type u_1} [inst : Group G] {H : Type u_2} [inst : 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 (_ : ∀ (a a_1 : G), f (a * a_1⁻¹) = f a * (f a_1)⁻¹)

@[simp]

theorem AddMonoidHom.coe_of_map_sub {G : Type u_2} [inst : AddGroup G] {H : Type u_1} [inst : AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :

↑(AddMonoidHom.ofMapSub f hf) = f

@[simp]

theorem MonoidHom.coe_of_map_div {G : Type u_2} [inst : Group G] {H : Type u_1} [inst : Group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :

↑(MonoidHom.ofMapDiv f hf) = f

def AddMonoidHom.instNegAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup.proof_1 {M : Type u_2} {G : Type u_1} [inst : AddZeroClass M] [inst : AddCommGroup G] (f : M →+ G) (a : M) (b : M) :

-↑f (a + b) = -↑f a + -↑f b

Equations

(_ : -↑f (a + b) = -↑f a + -↑f b) = (_ : -↑f (a + b) = -↑f a + -↑f b)

instance AddMonoidHom.instNegAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup {M : Type u_1} {G : Type u_2} [inst : AddZeroClass M] [inst : 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.instNegAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup = { neg := fun f => AddMonoidHom.mk' (fun g => -↑f g) (_ : ∀ (a b : M), -↑f (a + b) = -↑f a + -↑f b) }

instance MonoidHom.instInvMonoidHomToMulOneClassToMonoidToDivInvMonoidToGroup {M : Type u_1} {G : Type u_2} [inst : MulOneClass M] [inst : 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.instInvMonoidHomToMulOneClassToMonoidToDivInvMonoidToGroup = { inv := fun f => MonoidHom.mk' (fun g => (↑f g)⁻¹) (_ : ∀ (a b : M), (↑f (a * b))⁻¹ = (↑f a)⁻¹ * (↑f b)⁻¹) }

@[simp]

theorem AddMonoidHom.neg_apply {M : Type u_1} {G : Type u_2} :

∀ {x : AddZeroClass M} {x_1 : AddCommGroup G} (f : M →+ G) (x_2 : M), ↑(-f) x_2 = -↑f x_2

@[simp]

theorem MonoidHom.inv_apply {M : Type u_1} {G : Type u_2} :

∀ {x : MulOneClass M} {x_1 : CommGroup G} (f : M →* G) (x_2 : M), ↑f⁻¹ x_2 = (↑f x_2)⁻¹

@[simp]

theorem AddMonoidHom.neg_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup A} (φ : N →+ A) (ψ : M →+ N), AddMonoidHom.comp (-φ) ψ = -AddMonoidHom.comp φ ψ

@[simp]

theorem MonoidHom.inv_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} :

∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommGroup A} (φ : N →* A) (ψ : M →* N), MonoidHom.comp φ⁻¹ ψ = (MonoidHom.comp φ ψ)⁻¹

@[simp]

theorem AddMonoidHom.comp_neg {M : Type u_1} {A : Type u_2} {B : Type u_3} :

∀ {x : AddZeroClass M} {x_1 : AddCommGroup A} {x_2 : AddCommGroup B} (φ : A →+ B) (ψ : M →+ A), AddMonoidHom.comp φ (-ψ) = -AddMonoidHom.comp φ ψ

@[simp]

theorem MonoidHom.comp_inv {M : Type u_1} {A : Type u_2} {B : Type u_3} :

∀ {x : MulOneClass M} {x_1 : CommGroup A} {x_2 : CommGroup B} (φ : A →* B) (ψ : M →* A), MonoidHom.comp φ ψ⁻¹ = (MonoidHom.comp φ ψ)⁻¹

def AddMonoidHom.instSubAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup.proof_1 {M : Type u_2} {G : Type u_1} [inst : AddZeroClass M] [inst : AddCommGroup G] (f : M →+ G) (g : M →+ G) (a : M) (b : M) :

↑f (a + b) - ↑g (a + b) = ↑f a - ↑g a + (↑f b - ↑g b)

Equations

(_ : ↑f (a + b) - ↑g (a + b) = ↑f a - ↑g a + (↑f b - ↑g b)) = (_ : ↑f (a + b) - ↑g (a + b) = ↑f a - ↑g a + (↑f b - ↑g b))

instance AddMonoidHom.instSubAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup {M : Type u_1} {G : Type u_2} [inst : AddZeroClass M] [inst : 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

One or more equations did not get rendered due to their size.

instance MonoidHom.instDivMonoidHomToMulOneClassToMonoidToDivInvMonoidToGroup {M : Type u_1} {G : Type u_2} [inst : MulOneClass M] [inst : 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

One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.sub_apply {M : Type u_1} {G : Type u_2} :

∀ {x : AddZeroClass M} {x_1 : AddCommGroup G} (f g : M →+ G) (x_2 : M), ↑(f - g) x_2 = ↑f x_2 - ↑g x_2

@[simp]

theorem MonoidHom.div_apply {M : Type u_1} {G : Type u_2} :

∀ {x : MulOneClass M} {x_1 : CommGroup G} (f g : M →* G) (x_2 : M), ↑(f / g) x_2 = ↑f x_2 / ↑g x_2

instance instMulMonoidWithZeroHomToMulZeroOneClassToMonoidWithZero {M : Type u_1} {N : Type u_2} :

{x : MulZeroOneClass M} → [inst : CommMonoidWithZero N] → Mul (M →*₀ N)

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

Equations

One or more equations did not get rendered due to their size.