mathlib3 documentation

algebra.group.with_one.basic

More operations on with_one and with_zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines various bundled morphisms on with_one and with_zero that were not available in algebra/group/with_one/defs.

Main definitions #

@[simp]
theorem with_one.coe_mul_hom_apply {α : Type u} [has_mul α] (ᾰ : α) :
def with_zero.coe_add_hom {α : Type u} [has_add α] :

coe as a bundled morphism

Equations
@[simp]
theorem with_zero.coe_add_hom_apply {α : Type u} [has_add α] (ᾰ : α) :
def with_one.coe_mul_hom {α : Type u} [has_mul α] :

coe as a bundled morphism

Equations
def with_zero.lift {α : Type u} {β : Type v} [has_add α] [add_zero_class β] :
add_hom α β (with_zero α →+ β)

Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism.

Equations
def with_one.lift {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] :
→ₙ* β) (with_one α →* β)

Lift a semigroup homomorphism f to a bundled monoid homorphism.

Equations
@[simp]
theorem with_zero.lift_coe {α : Type u} {β : Type v} [has_add α] [add_zero_class β] (f : add_hom α β) (x : α) :
@[simp]
theorem with_one.lift_coe {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] (f : α →ₙ* β) (x : α) :
@[simp]
theorem with_zero.lift_zero {α : Type u} {β : Type v} [has_add α] [add_zero_class β] (f : add_hom α β) :
@[simp]
theorem with_one.lift_one {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] (f : α →ₙ* β) :
def with_one.map {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) :

Given a multiplicative map from α → β returns a monoid homomorphism from with_one α to with_one β

Equations
def with_zero.map {α : Type u} {β : Type v} [has_add α] [has_add β] (f : add_hom α β) :

Given an additive map from α → β returns an add_monoid homomorphism from with_zero α to with_zero β

Equations
@[simp]
theorem with_one.map_coe {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) (a : α) :
@[simp]
theorem with_zero.map_coe {α : Type u} {β : Type v} [has_add α] [has_add β] (f : add_hom α β) (a : α) :
@[simp]
theorem with_one.map_map {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : with_one α) :
theorem with_zero.map_map {α : Type u} {β : Type v} {γ : Type w} [has_add α] [has_add β] [has_add γ] (f : add_hom α β) (g : add_hom β γ) (x : with_zero α) :
@[simp]
theorem with_zero.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_add α] [has_add β] [has_add γ] (f : add_hom α β) (g : add_hom β γ) :
@[simp]
theorem with_one.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
@[simp]
theorem mul_equiv.with_one_congr_apply {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) (ᾰ : with_one α) :
@[simp]
theorem add_equiv.with_zero_congr_apply {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) (ᾰ : with_zero α) :
def mul_equiv.with_one_congr {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :

A version of equiv.option_congr for with_one.

Equations
@[simp]
theorem mul_equiv.with_one_congr_symm {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :
@[simp]
theorem mul_equiv.with_one_congr_trans {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) :