algebra.group.with_one.defs

with_one.with_zero.has_repr = {repr := λ (o : with_zero α), with_one.with_zero.has_repr._match_1 o}
with_one.with_zero.has_repr._match_1 (option.some a) = "↑" ++ repr a
with_one.with_zero.has_repr._match_1 option.none = "0"

source

@[protected, instance]

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

has_repr (with_one α)

Equations

with_one.has_repr = {repr := λ (o : with_one α), with_one.has_repr._match_1 o}
with_one.has_repr._match_1 (option.some a) = "↑" ++ repr a
with_one.has_repr._match_1 option.none = "1"

source

@[protected, instance]

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

has_repr (with_zero α)

Equations

with_zero.has_repr = {repr := λ (o : with_zero α), with_zero.has_repr._match_1 o}
with_zero.has_repr._match_1 option.none = "1"
with_zero.has_repr._match_1 (option.some a) = "↑" ++ repr a

source

@[protected, instance]

def with_zero.monad :

monad with_zero

Equations

with_zero.monad = option.monad

source

@[protected, instance]

def with_one.monad :

monad with_one

Equations

with_one.monad = option.monad

source

@[protected, instance]

def with_one.has_one {α : Type u} :

has_one (with_one α)

Equations

with_one.has_one = {one := option.none α}

source

@[protected, instance]

def with_zero.has_zero {α : Type u} :

has_zero (with_zero α)

Equations

with_zero.has_zero = {zero := option.none α}

source

@[protected, instance]

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

has_add (with_zero α)

Equations

with_zero.has_add = {add := option.lift_or_get has_add.add}

source

@[protected, 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}

source

@[protected, instance]

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

has_inv (with_one α)

Equations

with_one.has_inv = {inv := λ (a : with_one α), option.map has_inv.inv a}

source

@[protected, instance]

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

has_neg (with_zero α)

Equations

with_zero.has_neg = {neg := λ (a : with_zero α), option.map has_neg.neg a}

source

@[protected, instance]

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

has_involutive_inv (with_one α)

Equations

with_one.has_involutive_inv = {inv := has_inv.inv with_one.has_inv, inv_inv := _}

source

@[protected, instance]

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

has_involutive_neg (with_zero α)

Equations

with_zero.has_involutive_neg = {neg := has_neg.neg with_zero.has_neg, neg_neg := _}

source

@[protected, instance]

def with_one.inv_one_class {α : Type u} [has_inv α] :

inv_one_class (with_one α)

Equations

with_one.inv_one_class = {one := 1, inv := has_inv.inv with_one.has_inv, inv_one := _}

source

@[protected, instance]

def with_zero.neg_zero_class {α : Type u} [has_neg α] :

neg_zero_class (with_zero α)

Equations

with_zero.neg_zero_class = {zero := 0, neg := has_neg.neg with_zero.has_neg, neg_zero := _}

source

@[protected, instance]

def with_one.inhabited {α : Type u} :

inhabited (with_one α)

Equations

with_one.inhabited = {default := 1}

source

@[protected, instance]

def with_zero.inhabited {α : Type u} :

inhabited (with_zero α)

Equations

with_zero.inhabited = {default := 0}

source

@[protected, instance]

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

nontrivial (with_one α)

source

@[protected, instance]

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

nontrivial (with_zero α)

source

@[protected, instance]

def with_zero.has_coe_t {α : Type u} :

has_coe_t α (with_zero α)

Equations

with_zero.has_coe_t = {coe := option.some α}

source

@[protected, instance]

def with_one.has_coe_t {α : Type u} :

has_coe_t α (with_one α)

Equations

with_one.has_coe_t = {coe := option.some α}

source

def with_zero.rec_zero_coe {α : Type u} {C : with_zero α → Sort u_1} (h₁ : C 0) (h₂ : Π (a : α), C ↑a) (n : with_zero α) :

C n

Recursor for with_zero using the preferred forms 0 and ↑a.

Equations

with_zero.rec_zero_coe h₁ h₂ = option.rec h₁ h₂

source

def with_one.rec_one_coe {α : Type u} {C : with_one α → Sort u_1} (h₁ : C 1) (h₂ : Π (a : α), C ↑a) (n : with_one α) :

C n

Recursor for with_one using the preferred forms 1 and ↑a.

Equations

with_one.rec_one_coe h₁ h₂ = option.rec h₁ h₂

source

def with_zero.unzero {α : Type u} {x : with_zero α} (hx : x ≠ 0) :

α

Deconstruct a x : with_zero α to the underlying value in α, given a proof that x ≠ 0.

Equations

with_zero.unzero hx = with_bot.unbot x hx

source

def with_one.unone {α : Type u} {x : with_one α} (hx : x ≠ 1) :

α

Deconstruct a x : with_one α to the underlying value in α, given a proof that x ≠ 1.

Equations

with_one.unone hx = with_bot.unbot x hx

source

@[simp]

theorem with_zero.unzero_coe {α : Type u} {x : α} (hx : ↑x ≠ 0) :

with_zero.unzero hx = x

source

@[simp]

theorem with_one.unone_coe {α : Type u} {x : α} (hx : ↑x ≠ 1) :

with_one.unone hx = x

source

@[simp]

theorem with_zero.coe_unzero {α : Type u} {x : with_zero α} (hx : x ≠ 0) :

↑(with_zero.unzero hx) = x

source

@[simp]

theorem with_one.coe_unone {α : Type u} {x : with_one α} (hx : x ≠ 1) :

↑(with_one.unone hx) = x

source

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

option.some a = ↑a

source

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

option.some a = ↑a

source

@[simp]

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

↑a ≠ 0

source

@[simp]

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

↑a ≠ 1

source

@[simp]

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

1 ≠ ↑a

source

@[simp]

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

0 ≠ ↑a

source

theorem with_one.ne_one_iff_exists {α : Type u} {x : with_one α} :

x ≠ 1 ↔ ∃ (a : α), ↑a = x

source

theorem with_zero.ne_zero_iff_exists {α : Type u} {x : with_zero α} :

x ≠ 0 ↔ ∃ (a : α), ↑a = x

source

@[protected, instance]

def with_zero.can_lift {α : Type u} :

can_lift (with_zero α) α coe (λ (a : with_zero α), a ≠ 0)

Equations

with_zero.can_lift = {prf := _}

source

@[protected, instance]

def with_one.can_lift {α : Type u} :

can_lift (with_one α) α coe (λ (a : with_one α), a ≠ 1)

Equations

with_one.can_lift = {prf := _}

source

@[simp, norm_cast]

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

↑a = ↑b ↔ a = b

source

@[simp, norm_cast]

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

↑a = ↑b ↔ a = b

source

@[protected]

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

P 1 → (∀ (a : α), P ↑a) → P x

source

@[protected]

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

P 0 → (∀ (a : α), P ↑a) → P x

source

@[protected, instance]

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

add_zero_class (with_zero α)

Equations

with_zero.add_zero_class = {zero := 0, add := has_add.add with_zero.has_add, zero_add := _, add_zero := _}

source

@[protected, instance]

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

mul_one_class (with_one α)

Equations

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

source

@[protected, instance]

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

add_monoid (with_zero α)

Equations

with_zero.add_monoid = {add := add_zero_class.add with_zero.add_zero_class, add_assoc := _, zero := add_zero_class.zero with_zero.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (with_zero α)), nsmul_zero' := _, nsmul_succ' := _}

source

@[protected, instance]

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

monoid (with_one α)

Equations

with_one.monoid = {mul := mul_one_class.mul with_one.mul_one_class, mul_assoc := _, one := mul_one_class.one with_one.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (with_one α)), npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

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

add_comm_monoid (with_zero α)

Equations

with_zero.add_comm_monoid = {add := add_monoid.add with_zero.add_monoid, add_assoc := _, zero := add_monoid.zero with_zero.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul with_zero.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, 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 := _, npow := monoid.npow with_one.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[simp, norm_cast]

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

↑(a * b) = ↑a * ↑b

source

@[simp, norm_cast]

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

↑(a + b) = ↑a + ↑b

source

@[simp, norm_cast]

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

↑a⁻¹ = (↑a)⁻¹

source

@[simp, norm_cast]

theorem with_zero.coe_neg {α : Type u} [has_neg α] (a : α) :

↑-a = -↑a

source

@[protected, instance]

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

has_one (with_zero α)

Equations

with_zero.has_one = {one := ↑1}

source

@[simp, norm_cast]

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

↑1 = 1

source

@[protected, instance]

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

mul_zero_class (with_zero α)

Equations

with_zero.mul_zero_class = {mul := option.map₂ has_mul.mul, zero := 0, zero_mul := _, mul_zero := _}

source

@[simp, norm_cast]

theorem with_zero.coe_mul {α : Type u} [has_mul α] {a b : α} :

↑(a * b) = ↑a * ↑b

source

@[protected, instance]

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

no_zero_divisors (with_zero α)

source

@[protected, instance]

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

semigroup_with_zero (with_zero α)

Equations

with_zero.semigroup_with_zero = {mul := mul_zero_class.mul with_zero.mul_zero_class, mul_assoc := _, zero := mul_zero_class.zero with_zero.mul_zero_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

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

comm_semigroup (with_zero α)

Equations

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

source

@[protected, instance]

def with_zero.mul_zero_one_class {α : Type u} [mul_one_class α] :

mul_zero_one_class (with_zero α)

Equations

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

source

@[protected, instance]

def with_zero.nat.has_pow {α : Type u} [has_one α] [has_pow α ℕ] :

has_pow (with_zero α) ℕ

Equations

with_zero.nat.has_pow = {pow := λ (x : with_zero α) (n : ℕ), with_zero.nat.has_pow._match_1 x n}
with_zero.nat.has_pow._match_1 (option.some x) n = ↑(x ^ n)
with_zero.nat.has_pow._match_1 option.none (n + 1) = 0
with_zero.nat.has_pow._match_1 option.none 0 = 1

source

@[simp, norm_cast]

theorem with_zero.coe_pow {α : Type u} [has_one α] [has_pow α ℕ] {a : α} (n : ℕ) :

↑(a ^ n) = ↑a ^ n

source

@[protected, instance]

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

monoid_with_zero (with_zero α)

Equations

with_zero.monoid_with_zero = {mul := mul_zero_one_class.mul with_zero.mul_zero_one_class, mul_assoc := _, one := mul_zero_one_class.one with_zero.mul_zero_one_class, one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : with_zero α), x ^ n, npow_zero' := _, npow_succ' := _, zero := mul_zero_one_class.zero with_zero.mul_zero_one_class, zero_mul := _, mul_zero := _}

source

@[protected, 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 := _, npow := monoid_with_zero.npow with_zero.monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := monoid_with_zero.zero with_zero.monoid_with_zero, zero_mul := _, mul_zero := _}

source

@[protected, instance]

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

has_inv (with_zero α)

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

Equations

with_zero.has_inv = {inv := λ (a : with_zero α), option.map has_inv.inv a}

source

@[simp, norm_cast]

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

↑a⁻¹ = (↑a)⁻¹

source

@[simp]

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

0⁻¹ = 0

source

@[protected, instance]

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

has_involutive_inv (with_zero α)

Equations

with_zero.has_involutive_inv = {inv := has_inv.inv with_zero.has_inv, inv_inv := _}

source

@[protected, instance]

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

inv_one_class (with_zero α)

Equations

with_zero.inv_one_class = {one := 1, inv := has_inv.inv with_zero.has_inv, inv_one := _}

source

@[protected, instance]

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

has_div (with_zero α)

Equations

with_zero.has_div = {div := option.map₂ has_div.div}

source

@[norm_cast]

theorem with_zero.coe_div {α : Type u} [has_div α] (a b : α) :

↑(a / b) = ↑a / ↑b

source

@[protected, instance]

def with_zero.int.has_pow {α : Type u} [has_one α] [has_pow α ℤ] :

has_pow (with_zero α) ℤ

Equations

with_zero.int.has_pow = {pow := λ (x : with_zero α) (n : ℤ), with_zero.int.has_pow._match_1 x n}
with_zero.int.has_pow._match_1 (option.some x) n = ↑(x ^ n)
with_zero.int.has_pow._match_1 option.none -[1+ n] = 0
with_zero.int.has_pow._match_1 option.none (int.of_nat n.succ) = 0
with_zero.int.has_pow._match_1 option.none (int.of_nat 0) = 1