mathlib documentation

algebra.group.with_one

def with_one (α : Type u_1) :

Type u_1

Add an extra element 1 to a type

Equations

with_one α = option α

def with_zero (α : Type u_1) :

Type u_1

Add an extra element 0 to a type

@[instance]

def with_zero.monad :

monad with_zero

@[instance]

def with_one.monad :

Equations

with_one.monad = option.monad

@[instance]

def with_one.has_one {α : Type u} :

has_one (with_one α)

Equations

with_one.has_one = {one := none α}

@[instance]

def with_zero.has_zero {α : Type u} :

has_zero (with_zero α)

@[instance]

def with_one.inhabited {α : Type u} :

inhabited (with_one α)

Equations

with_one.inhabited = {default := 1}

@[instance]

def with_zero.inhabited {α : Type u} :

inhabited (with_zero α)

@[instance]

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

nontrivial (with_one α)

@[instance]

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

nontrivial (with_zero α)

@[instance]

def with_zero.has_coe_t {α : Type u} :

has_coe_t α (with_zero α)

@[instance]

def with_one.has_coe_t {α : Type u} :

has_coe_t α (with_one α)

Equations

with_one.has_coe_t = {coe := some α}

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 : α} :

@[simp]

theorem with_one.coe_ne_one {α : Type u} {a : α} :

@[simp]

theorem with_one.one_ne_coe {α : Type u} {a : α} :

@[simp]

theorem with_zero.zero_ne_coe {α : Type u} {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

theorem with_one.coe_inj {α : Type u} {a b : α} :

↑a = ↑b ↔ a = b

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 α) (a : P 1) (a_1 : ∀ (a : α), P ↑a) :

P x

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

P x

@[instance]

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

has_add (with_zero α)

@[instance]

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

has_mul (with_one α)

Equations

with_one.has_mul = {mul := option.lift_or_get has_mul.mul}

@[instance]

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

add_monoid (with_zero α)

@[instance]

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

monoid (with_one α)

Equations

with_one.monoid = {mul := has_mul.mul with_one.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}

@[instance]

def with_zero.add_comm_monoid {α : Type u} [add_comm_semigroup α] :

add_comm_monoid (with_zero α)

@[instance]

def with_one.comm_monoid {α : Type u} [comm_semigroup α] :

comm_monoid (with_one α)

Equations

with_one.comm_monoid = {mul := monoid.mul with_one.monoid, mul_assoc := _, one := monoid.one with_one.monoid, one_mul := _, mul_one := _, mul_comm := _}

def with_zero.lift {α : Type u} [add_semigroup α] {β : Type v} [add_monoid β] (f : α → β) (hf : ∀ (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 : α → β) (hf : ∀ (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

with_one.lift f hf = {to_fun := λ (x : with_one α), option.cases_on x 1 f, map_one' := _, map_mul' := _}

@[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 α →+ β) :

f = with_zero.lift (⇑f ∘ coe) _

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

f = with_one.lift (⇑f ∘ coe) _

def with_one.map {α : Type u} {β : Type v} [semigroup α] [semigroup β] (f : α → β) (hf : ∀ (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

with_one.map f hf = with_one.lift (coe ∘ f) _

def with_zero.map {α : Type u} {β : Type v} [add_semigroup α] [add_semigroup β] (f : α → β) (hf : ∀ (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.has_one {α : Type u} [one : has_one α] :

has_one (with_zero α)

Equations

with_zero.has_one = {one := ↑1}

theorem with_zero.coe_one {α : Type u} [has_one α] :

↑1 = 1

@[instance]

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

mul_zero_class (with_zero α)

Equations

with_zero.mul_zero_class = {mul := λ (o₁ o₂ : with_zero α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a * b) o₂), zero := 0, zero_mul := _, mul_zero := _}

@[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

@[instance]

def with_zero.semigroup {α : Type u} [semigroup α] :

semigroup (with_zero α)

Equations

with_zero.semigroup = {mul := mul_zero_class.mul with_zero.mul_zero_class, mul_assoc := _}

@[instance]

def with_zero.comm_semigroup {α : Type u} [comm_semigroup α] :

comm_semigroup (with_zero α)

Equations

with_zero.comm_semigroup = {mul := semigroup.mul with_zero.semigroup, mul_assoc := _, mul_comm := _}

@[instance]

def with_zero.monoid_with_zero {α : Type u} [monoid α] :

monoid_with_zero (with_zero α)

Equations

with_zero.monoid_with_zero = {mul := mul_zero_class.mul with_zero.mul_zero_class, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero := mul_zero_class.zero with_zero.mul_zero_class, zero_mul := _, mul_zero := _}

@[instance]

def with_zero.comm_monoid_with_zero {α : Type u} [comm_monoid α] :

comm_monoid_with_zero (with_zero α)

Equations

with_zero.comm_monoid_with_zero = {mul := monoid_with_zero.mul with_zero.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, mul_comm := _, zero := monoid_with_zero.zero with_zero.monoid_with_zero, zero_mul := _, mul_zero := _}

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

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

Equations

x.inv = x >>= λ (a : α), return a⁻¹

@[instance]

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

has_inv (with_zero α)

Equations

with_zero.has_inv = {inv := with_zero.inv _inst_1}

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem with_zero.inv_zero {α : Type u} [has_inv α] :

@[simp]

theorem with_zero.inv_one {α : Type u} [group α] :

def with_zero.div {α : Type u} [group α] (x y : with_zero α) :

A division operation on with_zero α when α has an inverse operation

Equations

x.div y = x * y⁻¹

@[instance]

def with_zero.has_div {α : Type u} [group α] :

has_div (with_zero α)

Equations

with_zero.has_div = {div := with_zero.div _inst_1}

@[simp]

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

0 / a = 0

@[simp]

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

a / 0 = 0

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

↑a / ↑b = ↑a * b⁻¹

theorem with_zero.one_div {α : Type u} [group α] (x : with_zero α) :

1 / x = x⁻¹

@[simp]

theorem with_zero.div_one {α : Type u} [group α] (x : with_zero α) :

x / 1 = x

@[simp]

theorem with_zero.mul_right_inv {α : Type u} [group α] (x : with_zero α) (h : x ≠ 0) :

x * x⁻¹ = 1

@[simp]

theorem with_zero.mul_left_inv {α : Type u} [group α] (x : with_zero α) (h : x ≠ 0) :

x⁻¹ * x = 1

@[simp]

theorem with_zero.mul_inv_rev {α : Type u} [group α] (x y : with_zero α) :

(x * y)⁻¹ = y⁻¹ * x⁻¹

@[simp]

theorem with_zero.mul_div_cancel {α : Type u} [group α] {a b : with_zero α} (hb : b ≠ 0) :

a * b / b = a

@[simp]

theorem with_zero.div_mul_cancel {α : Type u} [group α] {a b : with_zero α} (hb : b ≠ 0) :

(a / b) * b = a

theorem with_zero.div_eq_iff_mul_eq {α : Type u} [group α] {a b c : with_zero α} (hb : b ≠ 0) :

a / b = c ↔ c * b = a

theorem with_zero.mul_inv_cancel {α : Type u} [group α] (a : with_zero α) (a_1 : a ≠ 0) :

a * a⁻¹ = 1

@[instance]

def with_zero.group_with_zero {α : Type u} [group α] :

group_with_zero (with_zero α)

if G is a group then with_zero G is a group with zero.

Equations

with_zero.group_with_zero = {mul := monoid_with_zero.mul with_zero.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, zero := monoid_with_zero.zero with_zero.monoid_with_zero, zero_mul := _, mul_zero := _, inv := has_inv.inv with_zero.has_inv, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

theorem with_zero.div_eq_div {α : Type u} [comm_group α] {a b c d : with_zero α} (hb : b ≠ 0) (hd : d ≠ 0) :

a / b = c / d ↔ a * d = b * c

theorem with_zero.mul_comm {α : Type u} [comm_group α] (a b : with_zero α) :

a * b = b * a

@[instance]

def with_zero.comm_group_with_zero {α : Type u} [comm_group α] :

comm_group_with_zero (with_zero α)

if G is a comm_group then with_zero G is a comm_group_with_zero.

Equations

with_zero.comm_group_with_zero = {mul := group_with_zero.mul with_zero.group_with_zero, mul_assoc := _, one := group_with_zero.one with_zero.group_with_zero, one_mul := _, mul_one := _, mul_comm := _, zero := group_with_zero.zero with_zero.group_with_zero, zero_mul := _, mul_zero := _, inv := group_with_zero.inv with_zero.group_with_zero, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

@[instance]

def with_zero.semiring {α : Type u} [semiring α] :

semiring (with_zero α)

Equations

with_zero.semiring = {add := add_comm_monoid.add with_zero.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_zero.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := mul_zero_class.mul with_zero.mul_zero_class, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}