Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module deprecated.group
! leanprover-community/mathlib commit 5a3e819569b0f12cbec59d740a2613018e7b8eec
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.TypeTags
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Algebra.Hom.Ring
import Mathlib.Algebra.Hom.Units

/-!
# Unbundled monoid and group homomorphisms

This file is deprecated, and is no longer imported by anything in mathlib other than other
deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled monoid and group homomorphisms. Instead of using
this file, please use `MonoidHom`, defined in `Algebra.Hom.Group`, with notation `→*`, for
morphisms between monoids or groups. For example use `φ : G →* H` to represent a group
homomorphism between multiplicative groups, and `ψ : A →+ B` to represent a group homomorphism

## Main Definitions

`IsMonoidHom` (deprecated), `IsGroupHom` (deprecated)

## Tags

IsGroupHom, IsMonoidHom

-/

universe u v

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v}

/-- Predicate for maps which preserve an addition. -/
structure IsAddHom: ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Add β] {f : α → β},
(∀ (x y : α), f (x + y) = f x + f y) → IsAddHom fIsAddHom {α: Type ?u.10α β: Type ?u.13β : Type _: Type (?u.10+1)Type _} [Add: Type ?u.16 → Type ?u.16Add α: Type ?u.10α] [Add: Type ?u.19 → Type ?u.19Add β: Type ?u.13β] (f: α → βf : α: Type ?u.10α → β: Type ?u.13β) : Prop: TypeProp where
/-- The proposition that `f` preserves addition. -/
map_add: ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Add β] {f : α → β},
IsAddHom f → ∀ (x y : α), f (x + y) = f x + f ymap_add : ∀ x: ?m.28x y: ?m.31y, f: α → βf (x: ?m.28x + y: ?m.31y) = f: α → βf x: ?m.28x + f: α → βf y: ?m.31y
#align is_add_hom IsAddHom: {α : Type u_1} → {β : Type u_2} → [inst : Add α] → [inst : Add β] → (α → β) → PropIsAddHom

/-- Predicate for maps which preserve a multiplication. -/
@[to_additive: {α : Type u_1} → {β : Type u_2} → [inst : Add α] → [inst : Add β] → (α → β) → Propto_additive]
structure IsMulHom: {α : Type u_1} → {β : Type u_2} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom {α: Type ?u.138α β: Type ?u.141β : Type _: Type (?u.141+1)Type _} [Mul: Type ?u.144 → Type ?u.144Mul α: Type ?u.138α] [Mul: Type ?u.147 → Type ?u.147Mul β: Type ?u.141β] (f: α → βf : α: Type ?u.138α → β: Type ?u.141β) : Prop: TypeProp where
/-- The proposition that `f` preserves multiplication. -/
map_mul: ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul : ∀ x: ?m.156x y: ?m.159y, f: α → βf (x: ?m.156x * y: ?m.159y) = f: α → βf x: ?m.156x * f: α → βf y: ?m.159y
#align is_mul_hom IsMulHom: {α : Type u_1} → {β : Type u_2} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom

namespace IsMulHom

variable [Mul: Type ?u.925 → Type ?u.925Mul α: Type uα] [Mul: Type ?u.429 → Type ?u.429Mul β: Type vβ] {γ: Type ?u.432γ : Type _: Type (?u.290+1)Type _} [Mul: Type ?u.435 → Type ?u.435Mul γ: Type ?u.290γ]

/-- The identity map preserves multiplication. -/
theorem id: ∀ {α : Type u} [inst : Mul α], IsMulHom _root_.idid : IsMulHom: {α : Type ?u.313} → {β : Type ?u.312} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom (id: {α : Sort ?u.359} → α → αid : α: Type uα → α: Type uα) :=
{ map_mul := fun _: ?m.390_ _: ?m.393_ => rfl: ∀ {α : Sort ?u.395} {a : α}, a = arfl }
#align is_mul_hom.id IsMulHom.id: ∀ {α : Type u} [inst : Mul α], IsMulHom _root_.idIsMulHom.id

/-- The composition of maps which preserve multiplication, also preserves multiplication. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {γ : Type u_1} [inst_2 : Add γ] {f : α → β} {g : β → γ},
theorem comp: ∀ {f : α → β} {g : β → γ}, IsMulHom f → IsMulHom g → IsMulHom (g ∘ f)comp {f: α → βf : α: Type uα → β: Type vβ} {g: β → γg : β: Type vβ → γ: Type ?u.432γ} (hf: IsMulHom fhf : IsMulHom: {α : Type ?u.447} → {β : Type ?u.446} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf) (hg: IsMulHom ghg : IsMulHom: {α : Type ?u.514} → {β : Type ?u.513} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom g: β → γg) : IsMulHom: {α : Type ?u.572} → {β : Type ?u.571} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom (g: β → γg ∘ f: α → βf) :=
{ map_mul := fun x: ?m.661x y: ?m.664y => byGoals accomplished! 🐙 α: Type uβ: Type vinst✝²: Mul αinst✝¹: Mul βγ: Type u_1inst✝: Mul γf: α → βg: β → γhf: IsMulHom fhg: IsMulHom gx, y: α(g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) ysimp only [Function.comp: {α : Sort ?u.689} → {β : Sort ?u.688} → {δ : Sort ?u.687} → (β → δ) → (α → β) → α → δFunction.comp, hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.701} {β : Type ?u.700} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul, hg: IsMulHom ghg.map_mul: ∀ {α : Type ?u.731} {β : Type ?u.730} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul]Goals accomplished! 🐙 }
#align is_mul_hom.comp IsMulHom.comp: ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] {γ : Type u_1} [inst_2 : Mul γ] {f : α → β} {g : β → γ},
IsMulHom f → IsMulHom g → IsMulHom (g ∘ f)IsMulHom.comp
#align is_add_hom.comp IsAddHom.comp: ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {γ : Type u_1} [inst_2 : Add γ] {f : α → β} {g : β → γ},

/-- A product of maps which preserve multiplication,
preserves multiplication when the target is commutative. -/
@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : AddSemigroup α] [inst_1 : AddCommSemigroup β] {f g : α → β},
"A sum of maps which preserves addition, preserves addition when the target
is commutative."]
theorem mul: ∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : CommSemigroup β] {f g : α → β},
IsMulHom f → IsMulHom g → IsMulHom fun a => f a * g amul {α: Type u_1α β: ?m.940β} [Semigroup: Type ?u.943 → Type ?u.943Semigroup α: ?m.937α] [CommSemigroup: Type ?u.946 → Type ?u.946CommSemigroup β: ?m.940β] {f: α → βf g: α → βg : α: ?m.937α → β: ?m.940β} (hf: IsMulHom fhf : IsMulHom: {α : Type ?u.958} → {β : Type ?u.957} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf)
(hg: IsMulHom ghg : IsMulHom: {α : Type ?u.1608} → {β : Type ?u.1607} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom g: α → βg) : IsMulHom: {α : Type ?u.1657} → {β : Type ?u.1656} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom fun a: ?m.1701a => f: α → βf a: ?m.1701a * g: α → βg a: ?m.1701a :=
{ map_mul := fun a: ?m.2843a b: ?m.2846b => byGoals accomplished! 🐙
α✝: Type uβ✝: Type vinst✝⁴: Mul α✝inst✝³: Mul β✝γ: Type ?u.931inst✝²: Mul γα: Type u_1β: Type u_2inst✝¹: Semigroup αinst✝: CommSemigroup βf, g: α → βhf: IsMulHom fhg: IsMulHom ga, b: αf (a * b) * g (a * b) = f a * g a * (f b * g b)simp only [hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.2871} {β : Type ?u.2870} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul, hg: IsMulHom ghg.map_mul: ∀ {α : Type ?u.2895} {β : Type ?u.2894} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul, mul_comm: ∀ {G : Type ?u.2911} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm, mul_assoc: ∀ {G : Type ?u.2921} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc, mul_left_comm: ∀ {G : Type ?u.2933} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)mul_left_comm]Goals accomplished! 🐙 }
#align is_mul_hom.mul IsMulHom.mul: ∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : CommSemigroup β] {f g : α → β},
IsMulHom f → IsMulHom g → IsMulHom fun a => f a * g aIsMulHom.mul

/-- The inverse of a map which preserves multiplication,
preserves multiplication when the target is commutative. -/
@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : AddCommGroup β] {f : α → β},
the target is commutative."]
theorem inv: ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : CommGroup β] {f : α → β},
IsMulHom f → IsMulHom fun a => (f a)⁻¹inv {α: ?m.3713α β: Type u_2β} [Mul: Type ?u.3719 → Type ?u.3719Mul α: ?m.3713α] [CommGroup: Type ?u.3722 → Type ?u.3722CommGroup β: ?m.3716β] {f: α → βf : α: ?m.3713α → β: ?m.3716β} (hf: IsMulHom fhf : IsMulHom: {α : Type ?u.3730} → {β : Type ?u.3729} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf) : IsMulHom: {α : Type ?u.3994} → {β : Type ?u.3993} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom fun a: ?m.4038a => (f: α → βf a: ?m.4038a)⁻¹ :=
{ map_mul := fun a: ?m.4339a b: ?m.4342b => (hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.4345} {β : Type ?u.4344} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul a: ?m.4339a b: ?m.4342b).symm: ∀ {α : Sort ?u.4352} {a b : α}, a = b → b = asymm ▸ mul_inv: ∀ {α : Type ?u.4364} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹mul_inv _: ?m.4365_ _: ?m.4365_ }
#align is_mul_hom.inv IsMulHom.inv: ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : CommGroup β] {f : α → β},
IsMulHom f → IsMulHom fun a => (f a)⁻¹IsMulHom.inv
#align is_add_hom.neg IsAddHom.neg: ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : AddCommGroup β] {f : α → β},

end IsMulHom

/-- Predicate for additive monoid homomorphisms
(deprecated -- use the bundled `MonoidHom` version). -/
Prop: TypeProp where
/-- The proposition that `f` preserves the additive identity. -/
map_zero: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β}, IsAddMonoidHom f → f 0 = 0map_zero : f: α → βf 0: ?m.47250 = 0: ?m.50450
#align is_add_monoid_hom IsAddMonoidHom: {α : Type u} → {β : Type v} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom

/-- Predicate for monoid homomorphisms (deprecated -- use the bundled `MonoidHom` version). -/
@[to_additive: {α : Type u} → {β : Type v} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → Propto_additive]
structure IsMonoidHom: {α : Type u} → {β : Type v} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom [MulOneClass: Type ?u.5398 → Type ?u.5398MulOneClass α: Type uα] [MulOneClass: Type ?u.5401 → Type ?u.5401MulOneClass β: Type vβ] (f: α → βf : α: Type uα → β: Type vβ) extends IsMulHom: {α : Type ?u.5410} → {β : Type ?u.5409} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf : Prop: TypeProp where
/-- The proposition that `f` preserves the multiplicative identity. -/
map_one: ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β}, IsMonoidHom f → f 1 = 1map_one : f: α → βf 1: ?m.58131 = 1: ?m.60481
#align is_monoid_hom IsMonoidHom: {α : Type u} → {β : Type v} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom

namespace MonoidHom

variable {M: Type ?u.6322M : Type _: Type (?u.6338+1)Type _} {N: Type ?u.6341N : Type _: Type (?u.6325+1)Type _} {mM: MulOneClass MmM : MulOneClass: Type ?u.6344 → Type ?u.6344MulOneClass M: Type ?u.7682M} {mN: MulOneClass NmN : MulOneClass: Type ?u.6331 → Type ?u.6331MulOneClass N: Type ?u.6325N}

/-- Interpret a map `f : M → N` as a homomorphism `M →* N`. -/
@[to_additive: {M : Type u_1} →
{N : Type u_2} → {mM : AddZeroClass M} → {mN : AddZeroClass N} → {f : M → N} → IsAddMonoidHom f → M →+ Nto_additive "Interpret a map `f : M → N` as a homomorphism `M →+ N`."]
def of: {f : M → N} → IsMonoidHom f → M →* Nof {f: M → Nf : M: Type ?u.6338M → N: Type ?u.6341N} (h: IsMonoidHom fh : IsMonoidHom: {α : Type ?u.6355} → {β : Type ?u.6354} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: M → Nf) : M: Type ?u.6338M →* N: Type ?u.6341N
where
toFun := f: M → Nf
map_one' := h: IsMonoidHom fh.2: ∀ {α : Type ?u.6904} {β : Type ?u.6903} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 12
map_mul' := h: IsMonoidHom fh.1: ∀ {α : Type ?u.6921} {β : Type ?u.6920} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → IsMulHom f1.1: ∀ {α : Type ?u.6929} {β : Type ?u.6928} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f y1
#align monoid_hom.of MonoidHom.of: {M : Type u_1} → {N : Type u_2} → {mM : MulOneClass M} → {mN : MulOneClass N} → {f : M → N} → IsMonoidHom f → M →* NMonoidHom.of
{N : Type u_2} → {mM : AddZeroClass M} → {mN : AddZeroClass N} → {f : M → N} → IsAddMonoidHom f → M →+ NAddMonoidHom.of

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {f : M → N} (hf : IsAddMonoidHom f),
theorem coe_of: ∀ {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} {f : M → N} (hf : IsMonoidHom f), ↑(of hf) = fcoe_of {f: M → Nf : M: Type ?u.7682M → N: Type ?u.7685N} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.7699} → {β : Type ?u.7698} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: M → Nf) : ⇑(MonoidHom.of: {M : Type ?u.7733} →
{N : Type ?u.7732} → {mM : MulOneClass M} → {mN : MulOneClass N} → {f : M → N} → IsMonoidHom f → M →* NMonoidHom.of hf: IsMonoidHom fhf) = f: M → Nf :=
rfl: ∀ {α : Sort ?u.8266} {a : α}, a = arfl
#align monoid_hom.coe_of MonoidHom.coe_of: ∀ {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} {f : M → N} (hf : IsMonoidHom f), ↑(of hf) = fMonoidHom.coe_of
#align add_monoid_hom.coe_of AddMonoidHom.coe_of: ∀ {M : Type u_1} {N : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {f : M → N} (hf : IsAddMonoidHom f),

theorem isMonoidHom_coe: ∀ {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} (f : M →* N), IsMonoidHom ↑fisMonoidHom_coe (f: M →* Nf : M: Type ?u.8382M →* N: Type ?u.8385N) : IsMonoidHom: {α : Type ?u.8411} → {β : Type ?u.8410} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom (f: M →* Nf : M: Type ?u.8382M → N: Type ?u.8385N) :=
{ map_mul := f: M →* Nf.map_mul: ∀ {M : Type ?u.9326} {N : Type ?u.9327} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a b : M),
↑f (a * b) = ↑f a * ↑f bmap_mul
map_one := f: M →* Nf.map_one: ∀ {M : Type ?u.9356} {N : Type ?u.9357} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), ↑f 1 = 1map_one }
#align monoid_hom.is_monoid_hom_coe MonoidHom.isMonoidHom_coe: ∀ {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} (f : M →* N), IsMonoidHom ↑fMonoidHom.isMonoidHom_coe

end MonoidHom

namespace MulEquiv

variable {M: Type ?u.9403M : Type _: Type (?u.9419+1)Type _} {N: Type ?u.9406N : Type _: Type (?u.9422+1)Type _} [MulOneClass: Type ?u.9409 → Type ?u.9409MulOneClass M: Type ?u.9403M] [MulOneClass: Type ?u.9412 → Type ?u.9412MulOneClass N: Type ?u.9406N]

/-- A multiplicative isomorphism preserves multiplication (deprecated). -/
theorem isMulHom: ∀ (h : M ≃* N), IsMulHom ↑hisMulHom (h: M ≃* Nh : M: Type ?u.9419M ≃* N: Type ?u.9422N) : IsMulHom: {α : Type ?u.9790} → {β : Type ?u.9789} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom h: M ≃* Nh :=
⟨h: M ≃* Nh.map_mul: ∀ {M : Type ?u.9938} {N : Type ?u.9939} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (x y : M), ↑f (x * y) = ↑f x * ↑f ymap_mul⟩
#align mul_equiv.is_mul_hom MulEquiv.isMulHom: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), IsMulHom ↑hMulEquiv.isMulHom

/-- A multiplicative bijection between two monoids is a monoid hom
(deprecated -- use `MulEquiv.toMonoidHom`). -/
monoid hom (deprecated). "]
theorem isMonoidHom: ∀ (h : M ≃* N), IsMonoidHom ↑hisMonoidHom (h: M ≃* Nh : M: Type ?u.10350M ≃* N: Type ?u.10353N) : IsMonoidHom: {α : Type ?u.10721} → {β : Type ?u.10720} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom h: M ≃* Nh :=
{ map_mul := h: M ≃* Nh.map_mul: ∀ {M : Type ?u.11175} {N : Type ?u.11176} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (x y : M),
↑f (x * y) = ↑f x * ↑f ymap_mul
map_one := h: M ≃* Nh.map_one: ∀ {M : Type ?u.11201} {N : Type ?u.11202} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), ↑h 1 = 1map_one }
#align mul_equiv.is_monoid_hom MulEquiv.isMonoidHom: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), IsMonoidHom ↑hMulEquiv.isMonoidHom

end MulEquiv

namespace IsMonoidHom

variable [MulOneClass: Type ?u.11295 → Type ?u.11295MulOneClass α: Type uα] [MulOneClass: Type ?u.11298 → Type ?u.11298MulOneClass β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.11259} → {β : Type ?u.11258} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf)

/-- A monoid homomorphism preserves multiplication. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f → ∀ (x y : α), f (x + y) = f x + f yto_additive "An additive monoid homomorphism preserves addition."]
theorem map_mul': ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul' (x: αx y: ?m.11341y) : f: α → βf (x: ?m.11338x * y: ?m.11341y) = f: α → βf x: ?m.11338x * f: α → βf y: ?m.11341y :=
hf: IsMonoidHom fhf.map_mul: ∀ {α : Type ?u.12048} {β : Type ?u.12047} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul x: αx y: αy
#align is_monoid_hom.map_mul IsMonoidHom.map_mul': ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ (x y : α), f (x * y) = f x * f yIsMonoidHom.map_mul'
IsAddMonoidHom f → ∀ (x y : α), f (x + y) = f x + f yIsAddMonoidHom.map_add'

/-- The inverse of a map which preserves multiplication,
preserves multiplication when the target is commutative. -/
@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : AddCommGroup β] {f : α → β},
when the target is commutative."]
theorem inv: ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : CommGroup β] {f : α → β},
IsMonoidHom f → IsMonoidHom fun a => (f a)⁻¹inv {α: Type u_1α β: ?m.12425β} [MulOneClass: Type ?u.12428 → Type ?u.12428MulOneClass α: ?m.12422α] [CommGroup: Type ?u.12431 → Type ?u.12431CommGroup β: ?m.12425β] {f: α → βf : α: ?m.12422α → β: ?m.12425β} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.12439} → {β : Type ?u.12438} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf) :
IsMonoidHom: {α : Type ?u.12580} → {β : Type ?u.12579} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom fun a: ?m.12598a => (f: α → βf a: ?m.12598a)⁻¹ :=
{ map_one := hf: IsMonoidHom fhf.map_one: ∀ {α : Type ?u.13251} {β : Type ?u.13250} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 1map_one.symm: ∀ {α : Sort ?u.13258} {a b : α}, a = b → b = asymm ▸ inv_one: ∀ {G : Type ?u.13266} [inst : InvOneClass G], 1⁻¹ = 1inv_one
map_mul := fun a: ?m.13167a b: ?m.13170b => (hf: IsMonoidHom fhf.map_mul: ∀ {α : Type ?u.13181} {β : Type ?u.13180} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul a: ?m.13167a b: ?m.13170b).symm: ∀ {α : Sort ?u.13188} {a b : α}, a = b → b = asymm ▸ mul_inv: ∀ {α : Type ?u.13200} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹mul_inv _: ?m.13201_ _: ?m.13201_ }
#align is_monoid_hom.inv IsMonoidHom.inv: ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : CommGroup β] {f : α → β},
IsMonoidHom f → IsMonoidHom fun a => (f a)⁻¹IsMonoidHom.inv
#align is_add_monoid_hom.neg IsAddMonoidHom.neg: ∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : AddCommGroup β] {f : α → β},

end IsMonoidHom

/-- A map to a group preserving multiplication is a monoid homomorphism. -/
homomorphism."]
theorem IsMulHom.to_isMonoidHom: ∀ [inst : MulOneClass α] [inst_1 : Group β] {f : α → β}, IsMulHom f → IsMonoidHom fIsMulHom.to_isMonoidHom [MulOneClass: Type ?u.13370 → Type ?u.13370MulOneClass α: Type uα] [Group: Type ?u.13373 → Type ?u.13373Group β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: IsMulHom fhf : IsMulHom: {α : Type ?u.13381} → {β : Type ?u.13380} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf) :
IsMonoidHom: {α : Type ?u.13810} → {β : Type ?u.13809} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf :=
{ map_one := mul_right_eq_self: ∀ {M : Type ?u.14338} [inst : LeftCancelMonoid M] {a b : M}, a * b = a ↔ b = 1mul_right_eq_self.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 <| byGoals accomplished! 🐙 α: Type uβ: Type vinst✝¹: MulOneClass αinst✝: Group βf: α → βhf: IsMulHom f?m.14380 hf * f 1 = ?m.14380 hfrw [α: Type uβ: Type vinst✝¹: MulOneClass αinst✝: Group βf: α → βhf: IsMulHom f?m.14380 hf * f 1 = ?m.14380 hf← hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.14383} {β : Type ?u.14382} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul,α: Type uβ: Type vinst✝¹: MulOneClass αinst✝: Group βf: α → βhf: IsMulHom ff (?m.14400 hf * 1) = f (?m.14400 hf)α: Type uβ: Type v[inst : MulOneClass α] → [inst_1 : Group β] → {f : α → β} → IsMulHom f → α α: Type uβ: Type vinst✝¹: MulOneClass αinst✝: Group βf: α → βhf: IsMulHom f?m.14380 hf * f 1 = ?m.14380 hfone_mul: ∀ {M : Type ?u.14411} [inst : MulOneClass M] (a : M), 1 * a = aone_mulα: Type uβ: Type vinst✝¹: MulOneClass αinst✝: Group βf: α → βhf: IsMulHom ff 1 = f 1]Goals accomplished! 🐙
map_mul := hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.14322} {β : Type ?u.14321} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul }
#align is_mul_hom.to_is_monoid_hom IsMulHom.to_isMonoidHom: ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : Group β] {f : α → β}, IsMulHom f → IsMonoidHom fIsMulHom.to_isMonoidHom

namespace IsMonoidHom

variable [MulOneClass: Type ?u.14733 → Type ?u.14733MulOneClass α: Type uα] [MulOneClass: Type ?u.14736 → Type ?u.14736MulOneClass β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ}

/-- The identity map is a monoid homomorphism. -/
theorem id: IsMonoidHom _root_.idid : IsMonoidHom: {α : Type ?u.14744} → {β : Type ?u.14743} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom (@id: {α : Sort ?u.14761} → α → αid α: Type uα) :=
{ map_one := rfl: ∀ {α : Sort ?u.14990} {a : α}, a = arfl
map_mul := fun _: ?m.14973_ _: ?m.14976_ => rfl: ∀ {α : Sort ?u.14978} {a : α}, a = arfl }
#align is_monoid_hom.id IsMonoidHom.id: ∀ {α : Type u} [inst : MulOneClass α], IsMonoidHom _root_.idIsMonoidHom.id

/-- The composite of two monoid homomorphisms is a monoid homomorphism. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
homomorphism."]
theorem comp: ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ {γ : Type u_1} [inst_2 : MulOneClass γ] {g : β → γ}, IsMonoidHom g → IsMonoidHom (g ∘ f)comp (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.15023} → {β : Type ?u.15022} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf) {γ: Type u_1γ} [MulOneClass: Type ?u.15058 → Type ?u.15058MulOneClass γ: ?m.15055γ] {g: β → γg : β: Type vβ → γ: ?m.15055γ} (hg: IsMonoidHom ghg : IsMonoidHom: {α : Type ?u.15066} → {β : Type ?u.15065} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom g: β → γg) :
IsMonoidHom: {α : Type ?u.15096} → {β : Type ?u.15095} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom (g: β → γg ∘ f: α → βf) :=
{ IsMulHom.comp: ∀ {α : Type ?u.15142} {β : Type ?u.15141} [inst : Mul α] [inst_1 : Mul β] {γ : Type ?u.15143} [inst_2 : Mul γ]
{f : α → β} {g : β → γ}, IsMulHom f → IsMulHom g → IsMulHom (g ∘ f)IsMulHom.comp hf: IsMonoidHom fhf.toIsMulHom: ∀ {α : Type ?u.15210} {β : Type ?u.15209} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → IsMulHom ftoIsMulHom hg: IsMonoidHom ghg.toIsMulHom: ∀ {α : Type ?u.15245} {β : Type ?u.15244} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → IsMulHom ftoIsMulHom with
map_one := show g: β → γg _: β_ = 1: ?m.158451 by rw [α: Type uβ: Type vinst✝²: MulOneClass αinst✝¹: MulOneClass βf: α → βhf: IsMonoidHom fγ: Type u_1inst✝: MulOneClass γg: β → γhg: IsMonoidHom gsrc✝:= IsMulHom.comp hf.toIsMulHom hg.toIsMulHom: IsMulHom (g ∘ f)g (f 1) = 1hf: IsMonoidHom fhf.map_one: ∀ {α : Type ?u.16103} {β : Type ?u.16102} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 1map_one,α: Type uβ: Type vinst✝²: MulOneClass αinst✝¹: MulOneClass βf: α → βhf: IsMonoidHom fγ: Type u_1inst✝: MulOneClass γg: β → γhg: IsMonoidHom gsrc✝:= IsMulHom.comp hf.toIsMulHom hg.toIsMulHom: IsMulHom (g ∘ f)g 1 = 1 α: Type uβ: Type vinst✝²: MulOneClass αinst✝¹: MulOneClass βf: α → βhf: IsMonoidHom fγ: Type u_1inst✝: MulOneClass γg: β → γhg: IsMonoidHom gsrc✝:= IsMulHom.comp hf.toIsMulHom hg.toIsMulHom: IsMulHom (g ∘ f)g (f 1) = 1hg: IsMonoidHom ghg.map_one: ∀ {α : Type ?u.16114} {β : Type ?u.16113} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 1map_oneα: Type uβ: Type vinst✝²: MulOneClass αinst✝¹: MulOneClass βf: α → βhf: IsMonoidHom fγ: Type u_1inst✝: MulOneClass γg: β → γhg: IsMonoidHom gsrc✝:= IsMulHom.comp hf.toIsMulHom hg.toIsMulHom: IsMulHom (g ∘ f)1 = 1]Goals accomplished! 🐙 }
#align is_monoid_hom.comp IsMonoidHom.comp: ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → ∀ {γ : Type u_1} [inst_2 : MulOneClass γ] {g : β → γ}, IsMonoidHom g → IsMonoidHom (g ∘ f)IsMonoidHom.comp
#align is_add_monoid_hom.comp IsAddMonoidHom.comp: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},

end IsMonoidHom

/-- Left multiplication in a ring is an additive monoid morphism. -/
theorem isAddMonoidHom_mul_left: ∀ {γ : Type u_1} [inst : NonUnitalNonAssocSemiring γ] (x : γ), IsAddMonoidHom fun y => x * yisAddMonoidHom_mul_left {γ: Type ?u.16200γ : Type _: Type (?u.16200+1)Type _} [NonUnitalNonAssocSemiring: Type ?u.16203 → Type ?u.16203NonUnitalNonAssocSemiring γ: Type ?u.16200γ] (x: γx : γ: Type ?u.16200γ) :
IsAddMonoidHom: {α : Type ?u.16209} → {β : Type ?u.16208} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom fun y: γy : γ: Type ?u.16200γ => x: γx * y: γy :=
{ map_zero := mul_zero: ∀ {M₀ : Type ?u.16860} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero x: γx
map_add := fun y: ?m.16781y z: ?m.16784z => mul_add: ∀ {R : Type ?u.16786} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add x: γx y: ?m.16781y z: ?m.16784z }

/-- Right multiplication in a ring is an additive monoid morphism. -/
theorem isAddMonoidHom_mul_right: ∀ {γ : Type u_1} [inst : NonUnitalNonAssocSemiring γ] (x : γ), IsAddMonoidHom fun y => y * xisAddMonoidHom_mul_right {γ: Type ?u.16887γ : Type _: Type (?u.16887+1)Type _} [NonUnitalNonAssocSemiring: Type ?u.16890 → Type ?u.16890NonUnitalNonAssocSemiring γ: Type ?u.16887γ] (x: γx : γ: Type ?u.16887γ) :
IsAddMonoidHom: {α : Type ?u.16896} → {β : Type ?u.16895} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom fun y: γy : γ: Type ?u.16887γ => y: γy * x: γx :=
{ map_zero := zero_mul: ∀ {M₀ : Type ?u.17547} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0zero_mul x: γx
map_add := fun y: ?m.17468y z: ?m.17471z => add_mul: ∀ {R : Type ?u.17473} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul y: ?m.17468y z: ?m.17471z x: γx }

/-- Predicate for additive group homomorphism (deprecated -- use bundled `MonoidHom`). -/
#align is_add_group_hom IsAddGroupHom: {α : Type u} → {β : Type v} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → PropIsAddGroupHom

/-- Predicate for group homomorphisms (deprecated -- use bundled `MonoidHom`). -/
@[to_additive: {α : Type u} → {β : Type v} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → Propto_additive]
structure IsGroupHom: {α : Type u} → {β : Type v} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom [Group: Type ?u.17963 → Type ?u.17963Group α: Type uα] [Group: Type ?u.17966 → Type ?u.17966Group β: Type vβ] (f: α → βf : α: Type uα → β: Type vβ) extends IsMulHom: {α : Type ?u.17975} → {β : Type ?u.17974} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf : Prop: TypeProp
#align is_group_hom IsGroupHom: {α : Type u} → {β : Type v} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom

theorem MonoidHom.isGroupHom: ∀ {G : Type u_1} {H : Type u_2} {x : Group G} {x_1 : Group H} (f : G →* H), IsGroupHom ↑fMonoidHom.isGroupHom {G: Type ?u.18456G H: Type ?u.18459H : Type _: Type (?u.18459+1)Type _} {_: Group G_ : Group: Type ?u.18462 → Type ?u.18462Group G: Type ?u.18456G} {_: Group H_ : Group: Type ?u.18465 → Type ?u.18465Group H: Type ?u.18459H} (f: G →* Hf : G: Type ?u.18456G →* H: Type ?u.18459H) :
IsGroupHom: {α : Type ?u.18697} → {β : Type ?u.18696} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom (f: G →* Hf : G: Type ?u.18456G → H: Type ?u.18459H) :=
{ map_mul := f: G →* Hf.map_mul: ∀ {M : Type ?u.19676} {N : Type ?u.19677} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a b : M),
↑f (a * b) = ↑f a * ↑f bmap_mul }
#align monoid_hom.is_group_hom MonoidHom.isGroupHom: ∀ {G : Type u_1} {H : Type u_2} {x : Group G} {x_1 : Group H} (f : G →* H), IsGroupHom ↑fMonoidHom.isGroupHom

theorem MulEquiv.isGroupHom: ∀ {G : Type u_1} {H : Type u_2} {x : Group G} {x_1 : Group H} (h : G ≃* H), IsGroupHom ↑hMulEquiv.isGroupHom {G: Type u_1G H: Type u_2H : Type _: Type (?u.19906+1)Type _} {_: Group G_ : Group: Type ?u.19912 → Type ?u.19912Group G: Type ?u.19906G} {_: Group H_ : Group: Type ?u.19915 → Type ?u.19915Group H: Type ?u.19909H} (h: G ≃* Hh : G: Type ?u.19906G ≃* H: Type ?u.19909H) :
IsGroupHom: {α : Type ?u.20333} → {β : Type ?u.20332} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom h: G ≃* Hh :=
{ map_mul := h: G ≃* Hh.map_mul: ∀ {M : Type ?u.20839} {N : Type ?u.20840} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (x y : M),
↑f (x * y) = ↑f x * ↑f ymap_mul }
#align mul_equiv.is_group_hom MulEquiv.isGroupHom: ∀ {G : Type u_1} {H : Type u_2} {x : Group G} {x_1 : Group H} (h : G ≃* H), IsGroupHom ↑hMulEquiv.isGroupHom

/-- Construct `IsGroupHom` from its only hypothesis. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
(∀ (x y : α), f (x + y) = f x + f y) → IsAddGroupHom fto_additive "Construct `IsAddGroupHom` from its only hypothesis."]
theorem IsGroupHom.mk': ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
(∀ (x y : α), f (x * y) = f x * f y) → IsGroupHom fIsGroupHom.mk' [Group: Type ?u.20901 → Type ?u.20901Group α: Type uα] [Group: Type ?u.20904 → Type ?u.20904Group β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: ∀ (x y : α), f (x * y) = f x * f yhf : ∀ x: ?m.20912x y: ?m.20915y, f: α → βf (x: ?m.20912x * y: ?m.20915y) = f: α → βf x: ?m.20912x * f: α → βf y: ?m.20915y) :
IsGroupHom: {α : Type ?u.21701} → {β : Type ?u.21700} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf :=
{ map_mul := hf: ∀ (x y : α), f (x * y) = f x * f yhf }
#align is_group_hom.mk' IsGroupHom.mk': ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
(∀ (x y : α), f (x * y) = f x * f y) → IsGroupHom fIsGroupHom.mk'
#align is_add_group_hom.mk' IsAddGroupHom.mk': ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
(∀ (x y : α), f (x + y) = f x + f y) → IsAddGroupHom fIsAddGroupHom.mk'

namespace IsGroupHom

variable [Group: Type ?u.23735 → Type ?u.23735Group α: Type uα] [Group: Type ?u.24324 → Type ?u.24324Group β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.22180} → {β : Type ?u.22179} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf)

open IsMulHom (map_mul)

theorem map_mul': ∀ (x y : α), f (x * y) = f x * f ymap_mul' : ∀ x: ?m.22209x y: ?m.22212y, f: α → βf (x: ?m.22209x * y: ?m.22212y) = f: α → βf x: ?m.22209x * f: α → βf y: ?m.22212y :=
hf: IsGroupHom fhf.toIsMulHom: ∀ {α : Type ?u.22997} {β : Type ?u.22996} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom.map_mul: ∀ {α : Type ?u.23015} {β : Type ?u.23014} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul
#align is_group_hom.map_mul IsGroupHom.map_mul': ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (x y : α), f (x * y) = f x * f yIsGroupHom.map_mul'

/-- A group homomorphism is a monoid homomorphism. -/
theorem to_isMonoidHom: IsMonoidHom fto_isMonoidHom : IsMonoidHom: {α : Type ?u.23399} → {β : Type ?u.23398} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf :=
hf: IsGroupHom fhf.toIsMulHom: ∀ {α : Type ?u.23647} {β : Type ?u.23646} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom.to_isMonoidHom: ∀ {α : Type ?u.23665} {β : Type ?u.23664} [inst : MulOneClass α] [inst_1 : Group β] {f : α → β},
IsMulHom f → IsMonoidHom fto_isMonoidHom
#align is_group_hom.to_is_monoid_hom IsGroupHom.to_isMonoidHom: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMonoidHom fIsGroupHom.to_isMonoidHom

/-- A group homomorphism sends 1 to 1. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β}, IsAddGroupHom f → f 0 = 0to_additive "An additive group homomorphism sends 0 to 0."]
theorem map_one: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → f 1 = 1map_one : f: α → βf 1: ?m.237761 = 1: ?m.239061 :=
hf: IsGroupHom fhf.to_isMonoidHom: ∀ {α : Type ?u.24051} {β : Type ?u.24050} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMonoidHom fto_isMonoidHom.map_one: ∀ {α : Type ?u.24069} {β : Type ?u.24068} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 1map_one
#align is_group_hom.map_one IsGroupHom.map_one: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → f 1 = 1IsGroupHom.map_one

/-- A group homomorphism sends inverses to inverses. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ (a : α), f (-a) = -f ato_additive "An additive group homomorphism sends negations to negations."]
theorem map_inv: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → ∀ (a : α), f a⁻¹ = (f a)⁻¹map_inv (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.24361} → {β : Type ?u.24360} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) (a: αa : α: Type uα) : f: α → βf a: αa⁻¹ = (f: α → βf a: αa)⁻¹ :=
eq_inv_of_mul_eq_one_left: ∀ {α : Type ?u.24507} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → a = b⁻¹eq_inv_of_mul_eq_one_left <| byGoals accomplished! 🐙 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf a⁻¹ * f a = 1rw [α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf a⁻¹ * f a = 1← hf: IsGroupHom fhf.map_mul: ∀ {α : Type ?u.24554} {β : Type ?u.24553} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul,α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf (a⁻¹ * a) = 1 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf a⁻¹ * f a = 1inv_mul_self: ∀ {G : Type ?u.24981} [inst : Group G] (a : G), a⁻¹ * a = 1inv_mul_self,α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf 1 = 1 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: αf a⁻¹ * f a = 1hf: IsGroupHom fhf.map_one: ∀ {α : Type ?u.25010} {β : Type ?u.25009} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → f 1 = 1map_oneα: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa: α1 = 1]Goals accomplished! 🐙
#align is_group_hom.map_inv IsGroupHom.map_inv: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → ∀ (a : α), f a⁻¹ = (f a)⁻¹IsGroupHom.map_inv
#align is_add_group_hom.map_neg IsAddGroupHom.map_neg: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ (a : α), f (-a) = -f aIsAddGroupHom.map_neg

@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ (a b : α), f (a - b) = f a - f bto_additive]
theorem map_div: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (a b : α), f (a / b) = f a / f bmap_div (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.25130} → {β : Type ?u.25129} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) (a: αa b: αb : α: Type uα) : f: α → βf (a: αa / b: αb) = f: α → βf a: αa / f: α → βf b: αb := byGoals accomplished! 🐙
α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf (a / b) = f a / f bsimp_rw [α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf (a / b) = f a / f bdiv_eq_mul_inv: ∀ {G : Type ?u.25438} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹div_eq_mul_inv,α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf (a * b⁻¹) = f a * (f b)⁻¹ α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf (a / b) = f a / f bhf: IsGroupHom fhf.map_mul: ∀ {α : Type ?u.25656} {β : Type ?u.25655} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul,α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf a * f b⁻¹ = f a * (f b)⁻¹ α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf: α → βhf✝, hf: IsGroupHom fa, b: αf (a / b) = f a / f bhf: IsGroupHom fhf.map_inv: ∀ {α : Type ?u.26095} {β : Type ?u.26094} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (a : α), f a⁻¹ = (f a)⁻¹map_invGoals accomplished! 🐙]Goals accomplished! 🐙
#align is_group_hom.map_div IsGroupHom.map_div: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (a b : α), f (a / b) = f a / f bIsGroupHom.map_div
#align is_add_group_hom.map_sub IsAddGroupHom.map_sub: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → ∀ (a b : α), f (a - b) = f a - f bIsAddGroupHom.map_sub

/-- The identity is a group homomorphism. -/
theorem id: ∀ {α : Type u} [inst : Group α], IsGroupHom _root_.idid : IsGroupHom: {α : Type ?u.26253} → {β : Type ?u.26252} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom (@id: {α : Sort ?u.26268} → α → αid α: Type uα) :=
{ map_mul := fun _: ?m.26507_ _: ?m.26510_ => rfl: ∀ {α : Sort ?u.26512} {a : α}, a = arfl }
#align is_group_hom.id IsGroupHom.id: ∀ {α : Type u} [inst : Group α], IsGroupHom _root_.idIsGroupHom.id

/-- The composition of two group homomorphisms is a group homomorphism. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
group homomorphism."]
theorem comp: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ {γ : Type u_1} [inst_2 : Group γ] {g : β → γ}, IsGroupHom g → IsGroupHom (g ∘ f)comp (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.26583} → {β : Type ?u.26582} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) {γ: Type u_1γ} [Group: Type ?u.26614 → Type ?u.26614Group γ: ?m.26611γ] {g: β → γg : β: Type vβ → γ: ?m.26611γ} (hg: IsGroupHom ghg : IsGroupHom: {α : Type ?u.26622} → {β : Type ?u.26621} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom g: β → γg) :
IsGroupHom: {α : Type ?u.26648} → {β : Type ?u.26647} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom (g: β → γg ∘ f: α → βf) :=
{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438{ IsMulHom.comp: ∀ {α : Type ?u.26691} {β : Type ?u.26690} [inst : Mul α] [inst_1 : Mul β] {γ : Type ?u.26692} [inst_2 : Mul γ]
{f : α → β} {g : β → γ}, IsMulHom f → IsMulHom g → IsMulHom (g ∘ f)IsMulHom.comp{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438 hf: IsGroupHom fhf{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438.toIsMulHom: ∀ {α : Type ?u.26759} {β : Type ?u.26758} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438 hg: IsGroupHom ghg{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438.toIsMulHom: ∀ {α : Type ?u.26792} {β : Type ?u.26791} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438 { IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438with{ IsMulHom.comp hf.toIsMulHom hg.toIsMulHom with }: IsGroupHom ?m.27438 }
#align is_group_hom.comp IsGroupHom.comp: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ {γ : Type u_1} [inst_2 : Group γ] {g : β → γ}, IsGroupHom g → IsGroupHom (g ∘ f)IsGroupHom.comp
#align is_add_group_hom.comp IsAddGroupHom.comp: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},

/-- A group homomorphism is injective iff its kernel is trivial. -/
@[to_additive: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 0 → a = 0)to_additive "An additive group homomorphism is injective if its kernel is trivial."]
theorem injective_iff: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 1 → a = 1)injective_iff {f: α → βf : α: Type uα → β: Type vβ} (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.27582} → {β : Type ?u.27581} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) :
Function.Injective: {α : Sort ?u.27611} → {β : Sort ?u.27610} → (α → β) → PropFunction.Injective f: α → βf ↔ ∀ a: ?m.27618a, f: α → βf a: ?m.27618a = 1: ?m.276241 → a: ?m.27618a = 1: ?m.277681 :=
⟨fun h: ?m.27925h _: ?m.27928_ => byGoals accomplished! 🐙 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = 1 → x✝ = 1rw [α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = 1 → x✝ = 1← hf: IsGroupHom fhf.map_one: ∀ {α : Type ?u.27989} {β : Type ?u.27988} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → f 1 = 1map_oneα: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = f 1 → x✝ = 1]α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = f 1 → x✝ = 1;α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = f 1 → x✝ = 1 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: Function.Injective fx✝: αf x✝ = 1 → x✝ = 1exact @h: Function.Injective fh _: α_ _: α_Goals accomplished! 🐙, fun h: ?m.27936h x: ?m.27939x y: ?m.27942y hxy: ?m.27945hxy =>
eq_of_div_eq_one: ∀ {α : Type ?u.27947} [inst : DivisionMonoid α] {a b : α}, a / b = 1 → a = beq_of_div_eq_one <| h: ?m.27936h _: α_ <| byGoals accomplished! 🐙 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf (x / y) = 1rwa [α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf (x / y) = 1hf: IsGroupHom fhf.map_div: ∀ {α : Type ?u.28031} {β : Type ?u.28030} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → ∀ (a b : α), f (a / b) = f a / f bmap_div,α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf x / f y = 1 α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf (x / y) = 1div_eq_one: ∀ {G : Type ?u.28062} [inst : Group G] {a b : G}, a / b = 1 ↔ a = bdiv_eq_oneα: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf x = f y]α: Type uβ: Type vinst✝¹: Group αinst✝: Group βf✝: α → βhf✝: IsGroupHom f✝f: α → βhf: IsGroupHom fh: ∀ (a : α), f a = 1 → a = 1x, y: αhxy: f x = f yf x = f y⟩
#align is_group_hom.injective_iff IsGroupHom.injective_iff: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β},
IsGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 1 → a = 1)IsGroupHom.injective_iff
#align is_add_group_hom.injective_iff IsAddGroupHom.injective_iff: ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddGroup β] {f : α → β},
IsAddGroupHom f → (Function.Injective f ↔ ∀ (a : α), f a = 0 → a = 0)IsAddGroupHom.injective_iff

/-- The product of group homomorphisms is a group homomorphism if the target is commutative. -/
@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f g : α → β},
"The sum of two additive group homomorphisms is an additive group homomorphism
if the target is commutative."]
theorem mul: ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f g : α → β},
IsGroupHom f → IsGroupHom g → IsGroupHom fun a => f a * g amul {α: Type u_1α β: ?m.28218β} [Group: Type ?u.28221 → Type ?u.28221Group α: ?m.28215α] [CommGroup: Type ?u.28224 → Type ?u.28224CommGroup β: ?m.28218β] {f: α → βf g: α → βg : α: ?m.28215α → β: ?m.28218β} (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.28236} → {β : Type ?u.28235} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) (hg: IsGroupHom ghg : IsGroupHom: {α : Type ?u.28268} → {β : Type ?u.28267} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom g: α → βg) :
IsGroupHom: {α : Type ?u.28289} → {β : Type ?u.28288} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom fun a: ?m.28305a => f: α → βf a: ?m.28305a * g: α → βg a: ?m.28305a :=
{ map_mul := (hf: IsGroupHom fhf.toIsMulHom: ∀ {α : Type ?u.29154} {β : Type ?u.29153} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom.mul: ∀ {α : Type ?u.29161} {β : Type ?u.29162} [inst : Semigroup α] [inst_1 : CommSemigroup β] {f g : α → β},
IsMulHom f → IsMulHom g → IsMulHom fun a => f a * g amul hg: IsGroupHom ghg.toIsMulHom: ∀ {α : Type ?u.29328} {β : Type ?u.29327} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom).map_mul: ∀ {α : Type ?u.29337} {β : Type ?u.29336} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul }
#align is_group_hom.mul IsGroupHom.mul: ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f g : α → β},
IsGroupHom f → IsGroupHom g → IsGroupHom fun a => f a * g aIsGroupHom.mul

/-- The inverse of a group homomorphism is a group homomorphism if the target is commutative. -/
@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f : α → β},
"The negation of an additive group homomorphism is an additive group homomorphism
if the target is commutative."]
theorem inv: ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f : α → β},
IsGroupHom f → IsGroupHom fun a => (f a)⁻¹inv {α: ?m.29461α β: Type u_2β} [Group: Type ?u.29467 → Type ?u.29467Group α: ?m.29461α] [CommGroup: Type ?u.29470 → Type ?u.29470CommGroup β: ?m.29464β] {f: α → βf : α: ?m.29461α → β: ?m.29464β} (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.29478} → {β : Type ?u.29477} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) :
IsGroupHom: {α : Type ?u.29510} → {β : Type ?u.29509} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom fun a: ?m.29526a => (f: α → βf a: ?m.29526a)⁻¹ :=
{ map_mul := hf: IsGroupHom fhf.toIsMulHom: ∀ {α : Type ?u.30044} {β : Type ?u.30043} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom.inv: ∀ {α : Type ?u.30051} {β : Type ?u.30052} [inst : Mul α] [inst_1 : CommGroup β] {f : α → β},
IsMulHom f → IsMulHom fun a => (f a)⁻¹inv.map_mul: ∀ {α : Type ?u.30067} {β : Type ?u.30066} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul }
#align is_group_hom.inv IsGroupHom.inv: ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : CommGroup β] {f : α → β},
IsGroupHom f → IsGroupHom fun a => (f a)⁻¹IsGroupHom.inv
#align is_add_group_hom.neg IsAddGroupHom.neg: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f : α → β},

end IsGroupHom

namespace RingHom

/-!
These instances look redundant, because `Deprecated.Ring` provides `IsRingHom` for a `→+*`.
Nevertheless these are harmless, and helpful for stripping out dependencies on `Deprecated.Ring`.
-/

variable {R: Type ?u.30135R : Type _: Type (?u.30135+1)Type _} {S: Type ?u.30128S : Type _: Type (?u.30128+1)Type _}

section

variable [NonAssocSemiring: Type ?u.30864 → Type ?u.30864NonAssocSemiring R: Type ?u.30135R] [NonAssocSemiring: Type ?u.30144 → Type ?u.30144NonAssocSemiring S: Type ?u.30138S]

theorem to_isMonoidHom: ∀ (f : R →+* S), IsMonoidHom ↑fto_isMonoidHom (f: R →+* Sf : R: Type ?u.30151R →+* S: Type ?u.30154S) : IsMonoidHom: {α : Type ?u.30180} → {β : Type ?u.30179} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: R →+* Sf :=
{ map_one := f: R →+* Sf.map_one: ∀ {α : Type ?u.30835} {β : Type ?u.30836} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f 1 = 1map_one
map_mul := f: R →+* Sf.map_mul: ∀ {α : Type ?u.30800} {β : Type ?u.30801} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α),
↑f (a * b) = ↑f a * ↑f bmap_mul }
#align ring_hom.to_is_monoid_hom RingHom.to_isMonoidHom: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S), IsMonoidHom ↑fRingHom.to_isMonoidHom

theorem to_isAddMonoidHom: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
IsAddMonoidHom ↑fto_isAddMonoidHom (f: R →+* Sf : R: Type ?u.30858R →+* S: Type ?u.30861S) : IsAddMonoidHom: {α : Type ?u.30887} → {β : Type ?u.30886} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom f: R →+* Sf :=
{ map_zero := f: R →+* Sf.map_zero: ∀ {α : Type ?u.31700} {β : Type ?u.31701} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f 0 = 0map_zero
map_add := f: R →+* Sf.map_add: ∀ {α : Type ?u.31665} {β : Type ?u.31666} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α),
↑f (a + b) = ↑f a + ↑f bmap_add }
#align ring_hom.to_is_add_monoid_hom RingHom.to_isAddMonoidHom: ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),

end

section

variable [Ring: Type ?u.31729 → Type ?u.31729Ring R: Type ?u.31723R] [Ring: Type ?u.31732 → Type ?u.31732Ring S: Type ?u.31726S]

theorem to_isAddGroupHom: ∀ (f : R →+* S), IsAddGroupHom ↑fto_isAddGroupHom (f: R →+* Sf : R: Type ?u.31739R →+* S: Type ?u.31742S) : IsAddGroupHom: {α : Type ?u.31808} → {β : Type ?u.31807} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → PropIsAddGroupHom f: R →+* Sf :=
{ map_add := f: R →+* Sf.map_add: ∀ {α : Type ?u.32358} {β : Type ?u.32359} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α),
↑f (a + b) = ↑f a + ↑f bmap_add }
#align ring_hom.to_is_add_group_hom RingHom.to_isAddGroupHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), IsAddGroupHom ↑fRingHom.to_isAddGroupHom

end

end RingHom

/-- Inversion is a group homomorphism if the group is commutative. -/
theorem Inv.isGroupHom: ∀ [inst : CommGroup α], IsGroupHom invInv.isGroupHom [CommGroup: Type ?u.32407 → Type ?u.32407CommGroup α: Type uα] : IsGroupHom: {α : Type ?u.32411} → {β : Type ?u.32410} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom (Inv.inv: {α : Type ?u.32433} → [self : Inv α] → α → αInv.inv : α: Type uα → α: Type uα) :=
{ map_mul := mul_inv: ∀ {α : Type ?u.32741} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹mul_inv }
#align inv.is_group_hom Inv.isGroupHom: ∀ {α : Type u} [inst : CommGroup α], IsGroupHom Inv.invInv.isGroupHom

/-- The difference of two additive group homomorphisms is an additive group
homomorphism if the target is commutative. -/
theorem IsAddGroupHom.sub: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f g : α → β},
(hg: IsAddGroupHom ghg : IsAddGroupHom: {α : Type ?u.32890} → {β : Type ?u.32889} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → PropIsAddGroupHom g: α → βg) : IsAddGroupHom: {α : Type ?u.32913} → {β : Type ?u.32912} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → PropIsAddGroupHom fun a: ?m.32931a => f: α → βf a: ?m.32931a - g: α → βg a: ?m.32931a := byGoals accomplished! 🐙
IsAddGroupHom f → IsAddGroupHom g → IsAddGroupHom fun a => f a + g aadd hg: IsAddGroupHom ghg.neg: ∀ {α : Type ?u.33323} {β : Type ?u.33324} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f : α → β},
#align is_add_group_hom.sub IsAddGroupHom.sub: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst_1 : AddCommGroup β] {f g : α → β},

namespace Units

variable {M: Type ?u.33408M : Type _: Type (?u.33812+1)Type _} {N: Type ?u.33815N : Type _: Type (?u.33411+1)Type _} [Monoid: Type ?u.33818 → Type ?u.33818Monoid M: Type ?u.33408M] [Monoid: Type ?u.33433 → Type ?u.33433Monoid N: Type ?u.33411N]

/-- The group homomorphism on units induced by a multiplicative morphism. -/
@[reducible]
def map': {f : M → N} → IsMonoidHom f → Mˣ →* Nˣmap' {f: M → Nf : M: Type ?u.33424M → N: Type ?u.33427N} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.33441} → {β : Type ?u.33440} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: M → Nf) : M: Type ?u.33424Mˣ →* N: Type ?u.33427Nˣ :=
map: {M : Type ?u.33695} → {N : Type ?u.33694} → [inst : Monoid M] → [inst_1 : Monoid N] → (M →* N) → Mˣ →* Nˣmap (MonoidHom.of: {M : Type ?u.33735} →
{N : Type ?u.33734} → {mM : MulOneClass M} → {mN : MulOneClass N} → {f : M → N} → IsMonoidHom f → M →* NMonoidHom.of hf: IsMonoidHom fhf)
#align units.map' Units.map': {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid N] → {f : M → N} → IsMonoidHom f → Mˣ →* NˣUnits.map'

@[simp]
theorem coe_map': ∀ {f : M → N} (hf : IsMonoidHom f) (x : Mˣ), ↑(↑(map' hf) x) = f ↑xcoe_map' {f: M → Nf : M: Type ?u.33812M → N: Type ?u.33815N} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.33829} → {β : Type ?u.33828} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: M → Nf) (x: Mˣx : M: Type ?u.33812Mˣ) : ↑((map': {M : Type ?u.35372} →
{N : Type ?u.35371} → [inst : Monoid M] → [inst_1 : Monoid N] → {f : M → N} → IsMonoidHom f → Mˣ →* Nˣmap' hf: IsMonoidHom fhf : M: Type ?u.33812Mˣ → N: Type ?u.33815Nˣ) x: Mˣx) = f: M → Nf x: Mˣx :=
rfl: ∀ {α : Sort ?u.37295} {a : α}, a = arfl
#align units.coe_map' Units.coe_map': ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {f : M → N} (hf : IsMonoidHom f) (x : Mˣ),
↑(↑(map' hf) x) = f ↑xUnits.coe_map'

theorem coe_isMonoidHom: IsMonoidHom fun x => ↑xcoe_isMonoidHom : IsMonoidHom: {α : Type ?u.37371} → {β : Type ?u.37370} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom (↑· : M: Type ?u.37358Mˣ → M: Type ?u.37358M) :=
(coeHom: (M : Type ?u.38809) → [inst : Monoid M] → Mˣ →* McoeHom M: Type ?u.37358M).isMonoidHom_coe: ∀ {M : Type ?u.38819} {N : Type ?u.38820} {mM : MulOneClass M} {mN : MulOneClass N} (f : M →* N), IsMonoidHom ↑fisMonoidHom_coe
#align units.coe_is_monoid_hom Units.coe_isMonoidHom: ∀ {M : Type u_1} [inst : Monoid M], IsMonoidHom fun x => ↑xUnits.coe_isMonoidHom

end Units

namespace IsUnit

variable {M: Type ?u.38869M : Type _: Type (?u.38869+1)Type _} {N: Type ?u.38854N : Type _: Type (?u.38854+1)Type _} [Monoid: Type ?u.38857 → Type ?u.38857Monoid M: Type ?u.38851M] [Monoid: Type ?u.38860 → Type ?u.38860Monoid N: Type ?u.38872N] {x: Mx : M: Type ?u.38851M}

theorem map': ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {f : M → N},
IsMonoidHom f → ∀ {x : M}, IsUnit x → IsUnit (f x)map' {f: M → Nf : M: Type ?u.38869M → N: Type ?u.38872N} (hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.38888} → {β : Type ?u.38887} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: M → Nf) {x: Mx : M: Type ?u.38869M} (h: IsUnit xh : IsUnit: {M : Type ?u.39104} → [inst : Monoid M] → M → PropIsUnit x: Mx) : IsUnit: {M : Type ?u.39126} → [inst : Monoid M] → M → PropIsUnit (f: M → Nf x: Mx) :=
h: IsUnit xh.map: ∀ {F : Type ?u.39155} {M : Type ?u.39156} {N : Type ?u.39157} [inst : Monoid M] [inst_1 : Monoid N]
[inst_2 : MonoidHomClass F M N] (f : F) {x : M}, IsUnit x → IsUnit (↑f x)map (MonoidHom.of: {M : Type ?u.39174} →
{N : Type ?u.39173} → {mM : MulOneClass M} → {mN : MulOneClass N} → {f : M → N} → IsMonoidHom f → M →* NMonoidHom.of hf: IsMonoidHom fhf)
#align is_unit.map' IsUnit.map': ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {f : M → N},
IsMonoidHom f → ∀ {x : M}, IsUnit x → IsUnit (f x)IsUnit.map'

end IsUnit

theorem Additive.isAddHom: ∀ [inst : Mul α] [inst_1 : Mul β] {f : α → β}, IsMulHom f → IsAddHom fAdditive.isAddHom [Mul: Type ?u.39290 → Type ?u.39290Mul α: Type uα] [Mul: Type ?u.39293 → Type ?u.39293Mul β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: IsMulHom fhf : IsMulHom: {α : Type ?u.39301} → {β : Type ?u.39300} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom f: α → βf) :
@IsAddHom: {α : Type ?u.39368} → {β : Type ?u.39367} → [inst : Add α] → [inst : Add β] → (α → β) → PropIsAddHom (Additive: Type ?u.39369 → Type ?u.39369Additive α: Type uα) (Additive: Type ?u.39370 → Type ?u.39370Additive β: Type vβ) _ _ f: α → βf :=
{ map_add := hf: IsMulHom fhf.map_mul: ∀ {α : Type ?u.39456} {β : Type ?u.39455} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul }

@IsMulHom: {α : Type ?u.39571} → {β : Type ?u.39570} → [inst : Mul α] → [inst : Mul β] → (α → β) → PropIsMulHom (Multiplicative: Type ?u.39572 → Type ?u.39572Multiplicative α: Type uα) (Multiplicative: Type ?u.39573 → Type ?u.39573Multiplicative β: Type vβ) _ _ f: α → βf :=
{ map_mul := hf: IsAddHom fhf.map_add: ∀ {α : Type ?u.39659} {β : Type ?u.39658} [inst : Add α] [inst_1 : Add β] {f : α → β},
IsAddHom f → ∀ (x y : α), f (x + y) = f x + f ymap_add }
#align multiplicative.is_mul_hom Multiplicative.isMulHom: ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {f : α → β}, IsAddHom f → IsMulHom fMultiplicative.isMulHom

-- defeq abuse
theorem Additive.isAddMonoidHom: ∀ [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β}, IsMonoidHom f → IsAddMonoidHom fAdditive.isAddMonoidHom [MulOneClass: Type ?u.39706 → Type ?u.39706MulOneClass α: Type uα] [MulOneClass: Type ?u.39709 → Type ?u.39709MulOneClass β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ}
(hf: IsMonoidHom fhf : IsMonoidHom: {α : Type ?u.39717} → {β : Type ?u.39716} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom f: α → βf) : @IsAddMonoidHom: {α : Type ?u.39750} → {β : Type ?u.39749} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom (Additive: Type ?u.39751 → Type ?u.39751Additive α: Type uα) (Additive: Type ?u.39752 → Type ?u.39752Additive β: Type vβ) _ _ f: α → βf :=
{ Additive.isAddHom: ∀ {α : Type ?u.39788} {β : Type ?u.39787} [inst : Mul α] [inst_1 : Mul β] {f : α → β}, IsMulHom f → IsAddHom fAdditive.isAddHom hf: IsMonoidHom fhf.toIsMulHom: ∀ {α : Type ?u.39833} {β : Type ?u.39832} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → IsMulHom ftoIsMulHom with map_zero := hf: IsMonoidHom fhf.map_one: ∀ {α : Type ?u.40567} {β : Type ?u.40566} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},
IsMonoidHom f → f 1 = 1map_one }
#align additive.is_add_monoid_hom Additive.isAddMonoidHom: ∀ {α : Type u} {β : Type v} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α → β},

theorem Multiplicative.isMonoidHom: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f → IsMonoidHom fMultiplicative.isMonoidHom [AddZeroClass: Type ?u.40588 → Type ?u.40588AddZeroClass α: Type uα] [AddZeroClass: Type ?u.40591 → Type ?u.40591AddZeroClass β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ}
(hf: IsAddMonoidHom fhf : IsAddMonoidHom: {α : Type ?u.40599} → {β : Type ?u.40598} → [inst : AddZeroClass α] → [inst : AddZeroClass β] → (α → β) → PropIsAddMonoidHom f: α → βf) : @IsMonoidHom: {α : Type ?u.40628} → {β : Type ?u.40627} → [inst : MulOneClass α] → [inst : MulOneClass β] → (α → β) → PropIsMonoidHom (Multiplicative: Type ?u.40629 → Type ?u.40629Multiplicative α: Type uα) (Multiplicative: Type ?u.40630 → Type ?u.40630Multiplicative β: Type vβ) _ _ f: α → βf :=
{ Multiplicative.isMulHom: ∀ {α : Type ?u.40666} {β : Type ?u.40665} [inst : Add α] [inst_1 : Add β] {f : α → β}, IsAddHom f → IsMulHom fMultiplicative.isMulHom hf: IsAddMonoidHom fhf.toIsAddHom: ∀ {α : Type ?u.40701} {β : Type ?u.40700} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},
IsAddMonoidHom f → f 0 = 0map_zero }
#align multiplicative.is_monoid_hom Multiplicative.isMonoidHom: ∀ {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f : α → β},

theorem Additive.isAddGroupHom: ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsAddGroupHom fAdditive.isAddGroupHom [Group: Type ?u.41200 → Type ?u.41200Group α: Type uα] [Group: Type ?u.41203 → Type ?u.41203Group β: Type vβ] {f: α → βf : α: Type uα → β: Type vβ} (hf: IsGroupHom fhf : IsGroupHom: {α : Type ?u.41211} → {β : Type ?u.41210} → [inst : Group α] → [inst : Group β] → (α → β) → PropIsGroupHom f: α → βf) :
@IsAddGroupHom: {α : Type ?u.41240} → {β : Type ?u.41239} → [inst : AddGroup α] → [inst : AddGroup β] → (α → β) → PropIsAddGroupHom (Additive: Type ?u.41241 → Type ?u.41241Additive α: Type uα) (Additive: Type ?u.41242 → Type ?u.41242Additive β: Type vβ) _ _ f: α → βf :=
{ map_add := hf: IsGroupHom fhf.toIsMulHom: ∀ {α : Type ?u.41748} {β : Type ?u.41747} [inst : Group α] [inst_1 : Group β] {f : α → β}, IsGroupHom f → IsMulHom ftoIsMulHom.map_mul: ∀ {α : Type ?u.41766} {β : Type ?u.41765} [inst : Mul α] [inst_1 : Mul β] {f : α → β},
IsMulHom f → ∀ (x y : α), f (x * y) = f x * f ymap_mul }