algebra.group.with_one - mathlib docs

source

def with_one (α : Type u_1) :

Type u_1

Add an extra element 1 to a type

Equations

with_one α = option α

source

def with_zero (α : Type u_1) :

Type u_1

Add an extra element 0 to a type

Equations

with_zero α = option α

source

@[protected, instance]

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

has_repr (with_zero α)

Equations

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 (some a) = "↑" ++ repr a
with_one.with_zero.has_repr._match_1 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 (some a) = "↑" ++ repr a
with_one.has_repr._match_1 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 none = "1"
with_zero.has_repr._match_1 (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 := none α}

source

@[protected, instance]

def with_zero.has_zero {α : Type u} :

has_zero (with_zero α)

Equations

with_zero.has_zero = {zero := 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.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 := some α}

source

@[protected, instance]

def with_one.has_coe_t {α : Type u} :

has_coe_t α (with_one α)

Equations

with_one.has_coe_t = {coe := some α}

source

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

some a = ↑a

source

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

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 α) α

Equations

with_zero.can_lift = {coe := coe coe_to_lift, cond := λ (a : with_zero α), a ≠ 0, prf := _}

source

@[protected, instance]

def with_one.can_lift {α : Type u} :

can_lift (with_one α) α

Equations

with_one.can_lift = {coe := coe coe_to_lift, cond := λ (a : with_one α), a ≠ 1, 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]

theorem with_one.coe_mul_hom_apply {α : Type u} [has_mul α] (ᾰ : α) :

⇑with_one.coe_mul_hom ᾰ = ↑ᾰ

source

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

add_hom α (with_zero α)

coe as a bundled morphism

Equations

with_zero.coe_add_hom = {to_fun := coe coe_to_lift, map_add' := _}

source

@[simp]

theorem with_zero.coe_add_hom_apply {α : Type u} [has_add α] (ᾰ : α) :

⇑with_zero.coe_add_hom ᾰ = ↑ᾰ

source

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

α →ₙ* with_one α

coe as a bundled morphism

Equations

with_one.coe_mul_hom = {to_fun := coe coe_to_lift, map_mul' := _}

source

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

with_zero.lift = {to_fun := λ (f : add_hom α β), {to_fun := λ (x : with_zero α), option.cases_on x 0 ⇑f, map_zero' := _, map_add' := _}, inv_fun := λ (F : with_zero α →+ β), F.to_add_hom.comp with_zero.coe_add_hom, left_inv := _, right_inv := _}

source

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

with_one.lift = {to_fun := λ (f : α →ₙ* β), {to_fun := λ (x : with_one α), option.cases_on x 1 ⇑f, map_one' := _, map_mul' := _}, inv_fun := λ (F : with_one α →* β), F.to_mul_hom.comp with_one.coe_mul_hom, left_inv := _, right_inv := _}

source

@[simp]

theorem with_zero.lift_coe {α : Type u} {β : Type v} [has_add α] [add_zero_class β] (f : add_hom α β) (x : α) :

⇑(⇑with_zero.lift f) ↑x = ⇑f x

source

@[simp]

theorem with_one.lift_coe {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] (f : α →ₙ* β) (x : α) :

⇑(⇑with_one.lift f) ↑x = ⇑f x

source

@[simp]

theorem with_zero.lift_zero {α : Type u} {β : Type v} [has_add α] [add_zero_class β] (f : add_hom α β) :

⇑(⇑with_zero.lift f) 0 = 0

source

@[simp]

theorem with_one.lift_one {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] (f : α →ₙ* β) :

⇑(⇑with_one.lift f) 1 = 1

source

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

f = ⇑with_zero.lift (f.to_add_hom.comp with_zero.coe_add_hom)

source

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

f = ⇑with_one.lift (f.to_mul_hom.comp with_one.coe_mul_hom)

source

def with_one.map {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) :

with_one α →* with_one β

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

Equations

with_one.map f = ⇑with_one.lift (with_one.coe_mul_hom.comp f)

source

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

with_zero α →+ with_zero β

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

Equations

with_zero.map f = ⇑with_zero.lift (with_zero.coe_add_hom.comp f)

source

@[simp]

theorem with_one.map_coe {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) (a : α) :

⇑(with_one.map f) ↑a = ↑(⇑f a)

source

@[simp]

theorem with_zero.map_coe {α : Type u} {β : Type v} [has_add α] [has_add β] (f : add_hom α β) (a : α) :

⇑(with_zero.map f) ↑a = ↑(⇑f a)

source

@[simp]

theorem with_zero.map_id {α : Type u} [has_add α] :

with_zero.map (add_hom.id α) = add_monoid_hom.id (with_zero α)

source

@[simp]

theorem with_one.map_id {α : Type u} [has_mul α] :

with_one.map (mul_hom.id α) = monoid_hom.id (with_one α)

source

theorem with_one.map_map {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : with_one α) :

⇑(with_one.map g) (⇑(with_one.map f) x) = ⇑(with_one.map (g.comp f)) x

source

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

⇑(with_zero.map g) (⇑(with_zero.map f) x) = ⇑(with_zero.map (g.comp f)) x

source

@[simp]

theorem with_zero.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_add α] [has_add β] [has_add γ] (f : add_hom α β) (g : add_hom β γ) :

with_zero.map (g.comp f) = (with_zero.map g).comp (with_zero.map f)

source

@[simp]

theorem with_one.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :

with_one.map (g.comp f) = (with_one.map g).comp (with_one.map f)

source

@[simp]

theorem mul_equiv.with_one_congr_apply {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) (ᾰ : with_one α) :

⇑(e.with_one_congr) ᾰ = ⇑(with_one.map e.to_mul_hom) ᾰ

source

@[simp]

theorem add_equiv.with_zero_congr_apply {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) (ᾰ : with_zero α) :

⇑(e.with_zero_congr) ᾰ = ⇑(with_zero.map e.to_add_hom) ᾰ

source

def add_equiv.with_zero_congr {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) :

with_zero α ≃+ with_zero β

A version of equiv.option_congr for with_zero.

Equations

e.with_zero_congr = {to_fun := ⇑(with_zero.map e.to_add_hom), inv_fun := ⇑(with_zero.map e.symm.to_add_hom), left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.with_one_congr {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :

with_one α ≃* with_one β

A version of equiv.option_congr for with_one.

Equations

e.with_one_congr = {to_fun := ⇑(with_one.map e.to_mul_hom), inv_fun := ⇑(with_one.map e.symm.to_mul_hom), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.with_one_congr_refl {α : Type u} [has_mul α] :

(mul_equiv.refl α).with_one_congr = mul_equiv.refl (with_one α)

source

@[simp]

theorem mul_equiv.with_one_congr_symm {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :

e.with_one_congr.symm = e.symm.with_one_congr

source

@[simp]

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

e₁.with_one_congr.trans e₂.with_one_congr = (e₁.trans e₂).with_one_congr

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 := λ (o₁ o₂ : with_zero α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a * b) o₂), 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

@[simp]

theorem with_zero.zero_mul {α : Type u} [has_mul α] (a : with_zero α) :

0 * a = 0

source

@[simp]

theorem with_zero.mul_zero {α : Type u} [has_mul α] (a : with_zero α) :

a * 0 = 0

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 (some x) n = ↑(x ^ n)
with_zero.nat.has_pow._match_1 none (n + 1) = 0
with_zero.nat.has_pow._match_1 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_div {α : Type u} [has_div α] :

has_div (with_zero α)

Equations

with_zero.has_div = {div := λ (o₁ o₂ : with_zero α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a / b) o₂)}

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 (some x) n = ↑(x ^ n)
with_zero.int.has_pow._match_1 none -[1+ n] = 0
with_zero.int.has_pow._match_1 none (int.of_nat n.succ) = 0
with_zero.int.has_pow._match_1 none (int.of_nat 0) = 1