mathlib documentation

algebra.group.with_one

def with_one  :
Type u_1Type u_1

Add an extra element 1 to a type

Equations
def with_zero  :
Type u_1Type u_1

Add an extra element 0 to a type

@[instance]

@[instance]
def with_one.has_one {α : Type u} :

Equations
@[instance]
def with_zero.has_zero {α : Type u} :

@[instance]
def with_one.inhabited {α : Type u} :

Equations
@[instance]
def with_zero.inhabited {α : Type u} :

@[instance]
def with_one.nontrivial {α : Type u} [nonempty α] :

@[instance]
def with_zero.nontrivial {α : Type u} [nonempty α] :

@[instance]
def with_zero.has_coe_t {α : Type u} :

@[instance]
def with_one.has_coe_t {α : Type u} :

Equations
theorem with_one.some_eq_coe {α : Type u} {a : α} :

theorem with_zero.some_eq_coe {α : Type u} {a : α} :

@[simp]
theorem with_zero.coe_ne_zero {α : Type u} {a : α} :
a 0

@[simp]
theorem with_one.coe_ne_one {α : Type u} {a : α} :
a 1

@[simp]
theorem with_one.one_ne_coe {α : Type u} {a : α} :
1 a

@[simp]
theorem with_zero.zero_ne_coe {α : Type u} {a : α} :
0 a

theorem with_one.ne_one_iff_exists {α : Type u} {x : with_one α} :
x 1 ∃ (a : α), a = x

theorem with_zero.ne_zero_iff_exists {α : Type u} {x : with_zero α} :
x 0 ∃ (a : α), a = x

@[instance]
def with_one.can_lift {α : Type u} :

Equations
@[simp]
theorem with_one.coe_inj {α : Type u} {a b : α} :
a = b a = b

@[simp]
theorem with_zero.coe_inj {α : Type u} {a b : α} :
a = b a = b

theorem with_one.cases_on {α : Type u} {P : with_one α → Prop} (x : with_one α) :
P 1(∀ (a : α), P a)P x

theorem with_zero.cases_on {α : Type u} {P : with_zero α → Prop} (x : with_zero α) :
P 0(∀ (a : α), P a)P x

@[instance]
def with_zero.has_add {α : Type u} [has_add α] :

@[instance]
def with_one.has_mul {α : Type u} [has_mul α] :

Equations
@[instance]
def with_zero.add_monoid {α : Type u} [add_semigroup α] :

@[instance]
def with_one.monoid {α : Type u} [semigroup α] :

Equations
@[instance]

def with_zero.lift {α : Type u} [add_semigroup α] {β : Type v} [add_monoid β] (f : α → β) :
(∀ (x y : α), f (x + y) = f x + f y)with_zero α →+ β

Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism. We have no bundled add_semigroup homomorphisms, so this function takes ∀ x y, f (x + y) = f x + f y as an explicit argument.

def with_one.lift {α : Type u} [semigroup α] {β : Type v} [monoid β] (f : α → β) :
(∀ (x y : α), f (x * y) = (f x) * f y)with_one α →* β

Lift a semigroup homomorphism f to a bundled monoid homorphism. We have no bundled semigroup homomorphisms, so this function takes ∀ x y, f (x * y) = f x * f y as an explicit argument.

Equations
@[simp]
theorem with_zero.lift_coe {α : Type u} [add_semigroup α] {β : Type v} [add_monoid β] (f : α → β) (hf : ∀ (x y : α), f (x + y) = f x + f y) (x : α) :
(with_zero.lift f hf) x = f x

@[simp]
theorem with_one.lift_coe {α : Type u} [semigroup α] {β : Type v} [monoid β] (f : α → β) (hf : ∀ (x y : α), f (x * y) = (f x) * f y) (x : α) :
(with_one.lift f hf) x = f x

@[simp]
theorem with_zero.lift_zero {α : Type u} [add_semigroup α] {β : Type v} [add_monoid β] (f : α → β) (hf : ∀ (x y : α), f (x + y) = f x + f y) :
(with_zero.lift f hf) 0 = 0

@[simp]
theorem with_one.lift_one {α : Type u} [semigroup α] {β : Type v} [monoid β] (f : α → β) (hf : ∀ (x y : α), f (x * y) = (f x) * f y) :
(with_one.lift f hf) 1 = 1

theorem with_zero.lift_unique {α : Type u} [add_semigroup α] {β : Type v} [add_monoid β] (f : with_zero α →+ β) :

theorem with_one.lift_unique {α : Type u} [semigroup α] {β : Type v} [monoid β] (f : with_one α →* β) :

def with_one.map {α : Type u} {β : Type v} [semigroup α] [semigroup β] (f : α → β) :
(∀ (x y : α), f (x * y) = (f x) * f y)with_one α →* with_one β

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

Equations
def with_zero.map {α : Type u} {β : Type v} [add_semigroup α] [add_semigroup β] (f : α → β) :
(∀ (x y : α), f (x + y) = f x + f y)with_zero α →+ with_zero β

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

@[simp]
theorem with_one.coe_mul {α : Type u} [has_mul α] (a b : α) :
a * b = (a) * b

@[simp]
theorem with_zero.coe_add {α : Type u} [has_add α] (a b : α) :
(a + b) = a + b

@[instance]
def with_zero.can_lift {α : Type u} :

Equations
@[instance]
def with_zero.has_one {α : Type u} [one : has_one α] :

Equations
@[simp]
theorem with_zero.coe_one {α : Type u} [has_one α] :
1 = 1

@[instance]
def with_zero.mul_zero_class {α : Type u} [has_mul α] :

Equations
@[simp]
theorem with_zero.coe_mul {α : Type u} [has_mul α] {a b : α} :
a * b = (a) * b

@[simp]
theorem with_zero.zero_mul {α : Type u} [has_mul α] (a : with_zero α) :
0 * a = 0

@[simp]
theorem with_zero.mul_zero {α : Type u} [has_mul α] (a : with_zero α) :
a * 0 = 0

def with_zero.inv {α : Type u} [has_inv α] :

Given an inverse operation on α there is an inverse operation on with_zero α sending 0 to 0

Equations
@[instance]
def with_zero.has_inv {α : Type u} [has_inv α] :

Equations
@[simp]
theorem with_zero.coe_inv {α : Type u} [has_inv α] (a : α) :

@[simp]
theorem with_zero.inv_zero {α : Type u} [has_inv α] :
0⁻¹ = 0

@[simp]
theorem with_zero.inv_one {α : Type u} [group α] :
1⁻¹ = 1

theorem with_zero.div_coe {α : Type u} [group α] (a b : α) :