def isMonoidHom₁ {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G → H) : Prop

Equations

• isMonoidHom₁ f = (f 1 = 1 ∧ ∀ (g g' : G), f (g * g') = f g * f g')

structure isMonoidHom₂ {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G → H) : Prop

• map_one : f 1 = 1
• map_mul : ∀ (g g' : G), f (g * g') = f g * f g'

theorem isMonoidHom₂.map_one {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] {f : G → H} (self : isMonoidHom₂ f) : f 1 = 1

theorem isMonoidHom₂.map_mul {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] {f : G → H} (self : isMonoidHom₂ f) (g : G) (g' : G) : f (g * g') = f g * f g'

theorem MonoidHom₁.ext_iff {G : Type} {H : Type} : ∀ {inst : Monoid G} {inst_1 : Monoid H} {x y : MonoidHom₁ G H}, x = y ↔ ↑x = ↑y

theorem MonoidHom₁.ext {G : Type} {H : Type} : ∀ {inst : Monoid G} {inst_1 : Monoid H} {x y : MonoidHom₁ G H}, ↑x = ↑y → x = y

structure MonoidHom₁ (G : Type) (H : Type) [Monoid G] [Monoid H] : Type

• toFun : G → H
• map_one : ↑self 1 = 1
• map_mul : ∀ (g g' : G), ↑self (g * g') = ↑self g * ↑self g'

theorem MonoidHom₁.map_one {G : Type} {H : Type} [Monoid G] [Monoid H] (self : MonoidHom₁ G H) : ↑self 1 = 1

theorem MonoidHom₁.map_mul {G : Type} {H : Type} [Monoid G] [Monoid H] (self : MonoidHom₁ G H) (g : G) (g' : G) : ↑self (g * g') = ↑self g * ↑self g'

instance instCoeFunMonoidHom₁Forall {G : Type} {H : Type} [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) fun (x : MonoidHom₁ G H) => G → H

Equations

• instCoeFunMonoidHom₁Forall = { coe := MonoidHom₁.toFun }

theorem AddMonoidHom₁.ext {G : Type} {H : Type} : ∀ {inst : AddMonoid G} {inst_1 : AddMonoid H} {x y : AddMonoidHom₁ G H}, ↑x = ↑y → x = y

theorem AddMonoidHom₁.ext_iff {G : Type} {H : Type} : ∀ {inst : AddMonoid G} {inst_1 : AddMonoid H} {x y : AddMonoidHom₁ G H}, x = y ↔ ↑x = ↑y

structure AddMonoidHom₁ (G : Type) (H : Type) [AddMonoid G] [AddMonoid H] : Type

• toFun : G → H
• map_zero : ↑self 0 = 0
• map_add : ∀ (g g' : G), ↑self (g + g') = ↑self g + ↑self g'

theorem AddMonoidHom₁.map_zero {G : Type} {H : Type} [AddMonoid G] [AddMonoid H] (self : AddMonoidHom₁ G H) : ↑self 0 = 0

theorem AddMonoidHom₁.map_add {G : Type} {H : Type} [AddMonoid G] [AddMonoid H] (self : AddMonoidHom₁ G H) (g : G) (g' : G) : ↑self (g + g') = ↑self g + ↑self g'

instance instCoeFunAddMonoidHom₁Forall {G : Type} {H : Type} [AddMonoid G] [AddMonoid H] : CoeFun (AddMonoidHom₁ G H) fun (x : AddMonoidHom₁ G H) => G → H

Equations

• instCoeFunAddMonoidHom₁Forall = { coe := AddMonoidHom₁.toFun }

theorem RingHom₁.ext_iff {R : Type} {S : Type} : ∀ {inst : Ring R} {inst_1 : Ring S} {x y : RingHom₁ R S}, x = y ↔ ↑x.toMonoidHom₁ = ↑y.toMonoidHom₁

theorem RingHom₁.ext {R : Type} {S : Type} : ∀ {inst : Ring R} {inst_1 : Ring S} {x y : RingHom₁ R S}, ↑x.toMonoidHom₁ = ↑y.toMonoidHom₁ → x = y

structure RingHom₁ (R : Type) (S : Type) [Ring R] [Ring S] extends MonoidHom₁ : Type

• toFun : R → S
• map_one : ↑self.toMonoidHom₁ 1 = 1
• map_mul : ∀ (g g' : R), ↑self.toMonoidHom₁ (g * g') = ↑self.toMonoidHom₁ g * ↑self.toMonoidHom₁ g'
• map_zero : ↑self.toMonoidHom₁ 0 = 0
• map_add : ∀ (g g' : R), ↑self.toMonoidHom₁ (g + g') = ↑self.toMonoidHom₁ g + ↑self.toMonoidHom₁ g'

class MonoidHomClass₁ (F : Type) (M : Type) (N : Type) [Monoid M] [Monoid N] : Type

• toFun : F → M → N
• map_one : ∀ (f : F), MonoidHomClass₁.toFun f 1 = 1
• map_mul : ∀ (f : F) (g g' : M), MonoidHomClass₁.toFun f (g * g') = MonoidHomClass₁.toFun f g * MonoidHomClass₁.toFun f g'

theorem MonoidHomClass₁.map_one {F : Type} {M : Type} {N : Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₁ F M N] (f : F), MonoidHomClass₁.toFun f 1 = 1

theorem MonoidHomClass₁.map_mul {F : Type} {M : Type} {N : Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₁ F M N] (f : F) (g g' : M), MonoidHomClass₁.toFun f (g * g') = MonoidHomClass₁.toFun f g * MonoidHomClass₁.toFun f g'

def badInst {M : Type} {N : Type} {F : Type} [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F fun (x : F) => M → N

Equations

• badInst = { coe := MonoidHomClass₁.toFun }

class MonoidHomClass₂ (F : Type) (M : outParam Type) (N : outParam Type) [Monoid M] [Monoid N] : Type

• toFun : F → M → N
• map_one : ∀ (f : F), ↑f 1 = 1
• map_mul : ∀ (f : F) (g g' : M), ↑f (g * g') = ↑f g * ↑f g'

theorem MonoidHomClass₂.map_one {F : Type} {M : outParam Type} {N : outParam Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₂ F M N] (f : F), ↑f 1 = 1

theorem MonoidHomClass₂.map_mul {F : Type} {M : outParam Type} {N : outParam Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₂ F M N] (f : F) (g g' : M), ↑f (g * g') = ↑f g * ↑f g'

instance instCoeFunForallOfMonoidHomClass₂ {M : Type} {N : Type} {F : Type} [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F fun (x : F) => M → N

Equations

• instCoeFunForallOfMonoidHomClass₂ = { coe := MonoidHomClass₂.toFun }

instance instMonoidHomClass₂MonoidHom₁ (M : Type) (N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N

Equations

• instMonoidHomClass₂MonoidHom₁ M N = { toFun := MonoidHom₁.toFun, map_one := ⋯, map_mul := ⋯ }

instance instMonoidHomClass₂RingHom₁ (R : Type) (S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S

Equations

• instMonoidHomClass₂RingHom₁ R S = { toFun := fun (f : RingHom₁ R S) => ↑f.toMonoidHom₁, map_one := ⋯, map_mul := ⋯ }

theorem map_inv_of_inv {M : Type} {N : Type} {F : Type} [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] (f : F) {m : M} {m' : M} (h : m * m' = 1) : ↑f m * ↑f m' = 1

class MonoidHomClass₃ (F : Type) (M : outParam Type) (N : outParam Type) [Monoid M] [Monoid N] extends DFunLike : Type

• coe : F → M → N
• coe_injective' : Function.Injective DFunLike.coe
• map_one : ∀ (f : F), f 1 = 1
• map_mul : ∀ (f : F) (g g' : M), f (g * g') = f g * f g'

theorem MonoidHomClass₃.map_one {F : Type} {M : outParam Type} {N : outParam Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₃ F M N] (f : F), f 1 = 1

theorem MonoidHomClass₃.map_mul {F : Type} {M : outParam Type} {N : outParam Type} : ∀ {inst : Monoid M} {inst_1 : Monoid N} [self : MonoidHomClass₃ F M N] (f : F) (g g' : M), f (g * g') = f g * f g'

instance instMonoidHomClass₃MonoidHom₁ (M : Type) (N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N

Equations

• instMonoidHomClass₃MonoidHom₁ M N = MonoidHomClass₃.mk ⋯ ⋯

theorem OrderPresHom.ext {α : Type} {β : Type} : ∀ {inst : LE α} {inst_1 : LE β} {x y : OrderPresHom α β}, x.toFun = y.toFun → x = y

theorem OrderPresHom.ext_iff {α : Type} {β : Type} : ∀ {inst : LE α} {inst_1 : LE β} {x y : OrderPresHom α β}, x = y ↔ x.toFun = y.toFun

structure OrderPresHom (α : Type) (β : Type) [LE α] [LE β] : Type

• toFun : α → β
• le_of_le : ∀ (a a' : α), a ≤ a' → self.toFun a ≤ self.toFun a'

theorem OrderPresHom.le_of_le {α : Type} {β : Type} [LE α] [LE β] (self : OrderPresHom α β) (a : α) (a' : α) : a ≤ a' → self.toFun a ≤ self.toFun a'

theorem OrderPresMonoidHom.ext_iff {M : Type} {N : Type} : ∀ {inst : Monoid M} {inst_1 : LE M} {inst_2 : Monoid N} {inst_3 : LE N} {x y : OrderPresMonoidHom M N}, x = y ↔ ↑x.toMonoidHom₁ = ↑y.toMonoidHom₁

theorem OrderPresMonoidHom.ext {M : Type} {N : Type} : ∀ {inst : Monoid M} {inst_1 : LE M} {inst_2 : Monoid N} {inst_3 : LE N} {x y : OrderPresMonoidHom M N}, ↑x.toMonoidHom₁ = ↑y.toMonoidHom₁ → x = y

structure OrderPresMonoidHom (M : Type) (N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends MonoidHom₁ : Type

• toFun : M → N
• map_one : ↑self.toMonoidHom₁ 1 = 1
• map_mul : ∀ (g g' : M), ↑self.toMonoidHom₁ (g * g') = ↑self.toMonoidHom₁ g * ↑self.toMonoidHom₁ g'
• le_of_le : ∀ (a a' : M), a ≤ a' → ↑self.toMonoidHom₁ a ≤ ↑self.toMonoidHom₁ a'

class OrderPresHomClass (F : Type) (α : outParam Type) (β : outParam Type) [LE α] [LE β] : Type

instance instOrderPresHomClassOrderPresHom (α : Type) (β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β

Equations

• instOrderPresHomClassOrderPresHom α β = { }

instance instOrderPresHomClassOrderPresMonoidHom (α : Type) (β : Type) [LE α] [Monoid α] [LE β] [Monoid β] : OrderPresHomClass (OrderPresMonoidHom α β) α β

Equations

• instOrderPresHomClassOrderPresMonoidHom α β = { }

instance instMonoidHomClass₃OrderPresMonoidHom (α : Type) (β : Type) [LE α] [Monoid α] [LE β] [Monoid β] : MonoidHomClass₃ (OrderPresMonoidHom α β) α β

Equations

• instMonoidHomClass₃OrderPresMonoidHom α β = sorryAx (MonoidHomClass₃ (OrderPresMonoidHom α β) α β)