Equations
@[instance]
Equations
@[instance]
Equations
- free_comm_ring.inhabited α = {default := 0}
Equations
theorem
free_comm_ring.induction_on
{α : Type u}
{C : free_comm_ring α → Prop}
(z : free_comm_ring α) :
C (-1) → (∀ (b : α), C (free_comm_ring.of b)) → (∀ (x y : free_comm_ring α), C x → C y → C (x + y)) → (∀ (x y : free_comm_ring α), C x → C y → C (x * y)) → C z
Lift a map α → R to a additive group homomorphism free_comm_ring α → R.
For a version producing a bundled homomorphism, see lift_hom.
Equations
- free_comm_ring.lift f = free_abelian_group.lift (λ (s : multiplicative (multiset α)), (multiset.map f s).prod)
@[simp]
theorem
free_comm_ring.lift_zero
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β) :
⇑(free_comm_ring.lift f) 0 = 0
@[simp]
theorem
free_comm_ring.lift_one
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β) :
⇑(free_comm_ring.lift f) 1 = 1
@[simp]
theorem
free_comm_ring.lift_of
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x : α) :
⇑(free_comm_ring.lift f) (free_comm_ring.of x) = f x
@[simp]
theorem
free_comm_ring.lift_add
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.lift f) (x + y) = ⇑(free_comm_ring.lift f) x + ⇑(free_comm_ring.lift f) y
@[simp]
theorem
free_comm_ring.lift_neg
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x : free_comm_ring α) :
⇑(free_comm_ring.lift f) (-x) = -⇑(free_comm_ring.lift f) x
@[simp]
theorem
free_comm_ring.lift_sub
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.lift f) (x - y) = ⇑(free_comm_ring.lift f) x - ⇑(free_comm_ring.lift f) y
@[simp]
theorem
free_comm_ring.lift_mul
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.lift f) (x * y) = ⇑(free_comm_ring.lift f) x * ⇑(free_comm_ring.lift f) y
def
free_comm_ring.lift_hom
{α : Type u}
{β : Type v}
[comm_ring β] :
(α → β) → free_comm_ring α →+* β
Lift of a map f : α → β to free_comm_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_comm_ring.lift_hom f = {to_fun := ⇑(free_comm_ring.lift f), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
@[simp]
theorem
free_comm_ring.lift_pow
{α : Type u}
{β : Type v}
[comm_ring β]
(f : α → β)
(x : free_comm_ring α)
(n : ℕ) :
⇑(free_comm_ring.lift f) (x ^ n) = ⇑(free_comm_ring.lift f) x ^ n
@[simp]
theorem
free_comm_ring.lift_comp_of
{α : Type u}
{β : Type v}
[comm_ring β]
(f : free_comm_ring α → β)
[is_ring_hom f] :
⇑(free_comm_ring.lift (f ∘ free_comm_ring.of)) = f
@[simp]
theorem
free_comm_ring.lift_hom_comp_of
{α : Type u}
{β : Type v}
[comm_ring β]
(f : free_comm_ring α →+* β) :
A map f : α → β produces a ring homomorphism free_comm_ring α → free_comm_ring β.
Equations
theorem
free_comm_ring.map_zero
{α : Type u}
{β : Type v}
(f : α → β) :
⇑(free_comm_ring.map f) 0 = 0
theorem
free_comm_ring.map_one
{α : Type u}
{β : Type v}
(f : α → β) :
⇑(free_comm_ring.map f) 1 = 1
theorem
free_comm_ring.map_of
{α : Type u}
{β : Type v}
(f : α → β)
(x : α) :
⇑(free_comm_ring.map f) (free_comm_ring.of x) = free_comm_ring.of (f x)
theorem
free_comm_ring.map_add
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.map f) (x + y) = ⇑(free_comm_ring.map f) x + ⇑(free_comm_ring.map f) y
theorem
free_comm_ring.map_neg
{α : Type u}
{β : Type v}
(f : α → β)
(x : free_comm_ring α) :
⇑(free_comm_ring.map f) (-x) = -⇑(free_comm_ring.map f) x
theorem
free_comm_ring.map_sub
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.map f) (x - y) = ⇑(free_comm_ring.map f) x - ⇑(free_comm_ring.map f) y
theorem
free_comm_ring.map_mul
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_comm_ring α) :
⇑(free_comm_ring.map f) (x * y) = ⇑(free_comm_ring.map f) x * ⇑(free_comm_ring.map f) y
theorem
free_comm_ring.map_pow
{α : Type u}
{β : Type v}
(f : α → β)
(x : free_comm_ring α)
(n : ℕ) :
⇑(free_comm_ring.map f) (x ^ n) = ⇑(free_comm_ring.map f) x ^ n
Equations
- x.is_supported s = (x ∈ ring.closure (free_comm_ring.of '' s))
theorem
free_comm_ring.is_supported_upwards
{α : Type u}
{x : free_comm_ring α}
{s t : set α} :
x.is_supported s → s ⊆ t → x.is_supported t
theorem
free_comm_ring.is_supported_add
{α : Type u}
{x y : free_comm_ring α}
{s : set α} :
x.is_supported s → y.is_supported s → (x + y).is_supported s
theorem
free_comm_ring.is_supported_neg
{α : Type u}
{x : free_comm_ring α}
{s : set α} :
x.is_supported s → (-x).is_supported s
theorem
free_comm_ring.is_supported_sub
{α : Type u}
{x y : free_comm_ring α}
{s : set α} :
x.is_supported s → y.is_supported s → (x - y).is_supported s
theorem
free_comm_ring.is_supported_mul
{α : Type u}
{x y : free_comm_ring α}
{s : set α} :
x.is_supported s → y.is_supported s → (x * y).is_supported s
Equations
- free_comm_ring.restriction s = free_comm_ring.lift_hom (λ (p : α), dite (p ∈ s) (λ (H : p ∈ s), free_comm_ring.of ⟨p, H⟩) (λ (H : p ∉ s), 0))
@[simp]
theorem
free_comm_ring.restriction_of
{α : Type u}
(s : set α)
[decidable_pred s]
(p : α) :
⇑(free_comm_ring.restriction s) (free_comm_ring.of p) = dite (p ∈ s) (λ (H : p ∈ s), free_comm_ring.of ⟨p, H⟩) (λ (H : p ∉ s), 0)
@[simp]
theorem
free_comm_ring.restriction_zero
{α : Type u}
(s : set α)
[decidable_pred s] :
⇑(free_comm_ring.restriction s) 0 = 0
@[simp]
theorem
free_comm_ring.restriction_one
{α : Type u}
(s : set α)
[decidable_pred s] :
⇑(free_comm_ring.restriction s) 1 = 1
@[simp]
theorem
free_comm_ring.restriction_add
{α : Type u}
(s : set α)
[decidable_pred s]
(x y : free_comm_ring α) :
⇑(free_comm_ring.restriction s) (x + y) = ⇑(free_comm_ring.restriction s) x + ⇑(free_comm_ring.restriction s) y
@[simp]
theorem
free_comm_ring.restriction_neg
{α : Type u}
(s : set α)
[decidable_pred s]
(x : free_comm_ring α) :
⇑(free_comm_ring.restriction s) (-x) = -⇑(free_comm_ring.restriction s) x
@[simp]
theorem
free_comm_ring.restriction_sub
{α : Type u}
(s : set α)
[decidable_pred s]
(x y : free_comm_ring α) :
⇑(free_comm_ring.restriction s) (x - y) = ⇑(free_comm_ring.restriction s) x - ⇑(free_comm_ring.restriction s) y
@[simp]
theorem
free_comm_ring.restriction_mul
{α : Type u}
(s : set α)
[decidable_pred s]
(x y : free_comm_ring α) :
⇑(free_comm_ring.restriction s) (x * y) = ⇑(free_comm_ring.restriction s) x * ⇑(free_comm_ring.restriction s) y
theorem
free_comm_ring.is_supported_of
{α : Type u}
{p : α}
{s : set α} :
(free_comm_ring.of p).is_supported s ↔ p ∈ s
theorem
free_comm_ring.map_subtype_val_restriction
{α : Type u}
{x : free_comm_ring α}
(s : set α)
[decidable_pred s] :
x.is_supported s → ⇑(free_comm_ring.map subtype.val) (⇑(free_comm_ring.restriction s) x) = x
theorem
free_comm_ring.exists_finite_support
{α : Type u}
(x : free_comm_ring α) :
∃ (s : set α), s.finite ∧ x.is_supported s
theorem
free_comm_ring.exists_finset_support
{α : Type u}
(x : free_comm_ring α) :
∃ (s : finset α), x.is_supported ↑s
@[instance]
Equations
@[simp]
def
free_ring.of'
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
(e : R ≃ S)
[is_ring_hom ⇑e] :
R ≃+* S
Interpret an equivalence f : R ≃ S as a ring equivalence R ≃+* S.
@[instance]
Equations
- free_ring.comm_ring α = {add := ring.add (free_ring.ring α), add_assoc := _, zero := ring.zero (free_ring.ring α), zero_add := _, add_zero := _, neg := ring.neg (free_ring.ring α), add_left_neg := _, add_comm := _, mul := ring.mul (free_ring.ring α), mul_assoc := _, one := ring.one (free_ring.ring α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
Equations
- free_comm_ring_equiv_mv_polynomial_int α = {to_fun := ⇑(free_comm_ring.lift (λ (a : α), mv_polynomial.X a)), inv_fun := mv_polynomial.eval₂ (int.cast_ring_hom (free_comm_ring α)) free_comm_ring.of, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}