@[instance]
Equations
- with_one.has_one = {one := option.none α}
@[instance]
Equations
- with_one.inhabited = {default := 1}
@[instance]
Equations
@[instance]
Equations
- with_one.has_coe_t = {coe := option.some α}
theorem
with_zero.cases_on
{α : Type u}
{P : with_zero α → Prop}
(x : with_zero α) :
P 0 → (∀ (a : α), P ↑a) → P x
theorem
with_one.cases_on
{α : Type u}
{P : with_one α → Prop}
(x : with_one α) :
P 1 → (∀ (a : α), P ↑a) → P x
@[instance]
Equations
@[instance]
@[instance]
Equations
- with_one.monoid = {mul := has_mul.mul with_one.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
@[instance]
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 := _}
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.
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.
@[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_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) _
Given an additive map from α → β returns an add_monoid homomorphism
from with_zero α to with_zero β
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) _
@[instance]
Equations
- with_zero.has_one = {one := ↑1}
@[instance]
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 := _}
@[instance]
Equations
@[instance]
Equations
- with_zero.comm_semigroup = {mul := semigroup.mul with_zero.semigroup, mul_assoc := _, mul_comm := _}
@[instance]
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]
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 := _}
@[instance]
Equations
- with_zero.has_inv = {inv := with_zero.inv _inst_1}
@[instance]
Equations
- with_zero.has_div = {div := with_zero.div _inst_1}
@[instance]
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 := _}
@[instance]
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]
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 := _}