@[instance]
Equations
@[instance]
Equations
- free_ring.inhabited α = {default := 0}
Equations
theorem
free_ring.induction_on
{α : Type u}
{C : free_ring α → Prop}
(z : free_ring α) :
C (-1) → (∀ (b : α), C (free_ring.of b)) → (∀ (x y : free_ring α), C x → C y → C (x + y)) → (∀ (x y : free_ring α), C x → C y → C (x * y)) → C z
Equations
- free_ring.lift f = ⇑(free_abelian_group.lift (λ (L : list α), (list.map f L).prod))
@[simp]
theorem
free_ring.lift_zero
{α : Type u}
{β : Type v}
[ring β]
(f : α → β) :
free_ring.lift f 0 = 0
@[simp]
@[simp]
theorem
free_ring.lift_of
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x : α) :
free_ring.lift f (free_ring.of x) = f x
@[simp]
theorem
free_ring.lift_add
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x y : free_ring α) :
free_ring.lift f (x + y) = free_ring.lift f x + free_ring.lift f y
@[simp]
theorem
free_ring.lift_neg
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x : free_ring α) :
free_ring.lift f (-x) = -free_ring.lift f x
@[simp]
theorem
free_ring.lift_sub
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x y : free_ring α) :
free_ring.lift f (x - y) = free_ring.lift f x - free_ring.lift f y
@[simp]
theorem
free_ring.lift_mul
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x y : free_ring α) :
free_ring.lift f (x * y) = free_ring.lift f x * free_ring.lift f y
@[instance]
Equations
- _ = _
@[simp]
theorem
free_ring.lift_pow
{α : Type u}
{β : Type v}
[ring β]
(f : α → β)
(x : free_ring α)
(n : ℕ) :
free_ring.lift f (x ^ n) = free_ring.lift f x ^ n
@[simp]
theorem
free_ring.lift_comp_of
{α : Type u}
{β : Type v}
[ring β]
(f : free_ring α →+* β) :
free_ring.lift (⇑f ∘ free_ring.of) = ⇑f
Lift of a map f : α → β to free_ring α as a ring homomorphism.
We don't use it as the canonical form because Lean fails to coerce it to a function.
Equations
- free_ring.lift_hom f = {to_fun := free_ring.lift f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Equations
@[simp]
@[simp]
@[simp]
theorem
free_ring.map_of
{α : Type u}
{β : Type v}
(f : α → β)
(x : α) :
free_ring.map f (free_ring.of x) = free_ring.of (f x)
@[simp]
theorem
free_ring.map_add
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_ring α) :
free_ring.map f (x + y) = free_ring.map f x + free_ring.map f y
@[simp]
theorem
free_ring.map_neg
{α : Type u}
{β : Type v}
(f : α → β)
(x : free_ring α) :
free_ring.map f (-x) = -free_ring.map f x
@[simp]
theorem
free_ring.map_sub
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_ring α) :
free_ring.map f (x - y) = free_ring.map f x - free_ring.map f y
@[simp]
theorem
free_ring.map_mul
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_ring α) :
free_ring.map f (x * y) = free_ring.map f x * free_ring.map f y
@[simp]
theorem
free_ring.map_pow
{α : Type u}
{β : Type v}
(f : α → β)
(x : free_ring α)
(n : ℕ) :
free_ring.map f (x ^ n) = free_ring.map f x ^ n