Zulip Chat Archive

Stream: general

Topic: something is taking 1 second


view this post on Zulip Kenny Lau (Jul 23 2018 at 13:12):

import linear_algebra.multivariate_polynomial

universes u

namespace mv_polynomial

variables {σ : Type*} [decidable_eq σ] {α : Type*} [decidable_eq α] [comm_ring α]

instance : comm_ring (mv_polynomial σ α) := finsupp.to_comm_ring

instance C_is_ring_hom : is_ring_hom (C : α  mv_polynomial σ α) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

end mv_polynomial
open mv_polynomial

noncomputable theory
local attribute [instance] classical.prop_decidable

-- def ℤpinv := {x ∈ ℚ | ∃ n : ℕ, ∃ y : ℤ, x * (p:ℚ)^n = y}
set_option profiler true
lemma functorial_C_X {R : Type u} [comm_ring R] : functorial (C : R  mv_polynomial  R) (X 0) = X 0 :=
begin
  simp [functorial,X]
end

#check 2

view this post on Zulip Kenny Lau (Jul 23 2018 at 13:13):

elaboration of functorial_C_X took 975ms

view this post on Zulip Johan Commelin (Jul 23 2018 at 13:17):

Over here it isn't even a proof...

view this post on Zulip Kenny Lau (Jul 23 2018 at 13:18):

that's just the first step

view this post on Zulip Johan Commelin (Jul 23 2018 at 13:18):

Ok


Last updated: May 09 2021 at 19:11 UTC