something is taking 1 second

Stream: general

[Kenny Lau]

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

[Kenny Lau]

elaboration of functorial_C_X took 975ms

[Johan Commelin]

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

[Kenny Lau]

that's just the first step

[Johan Commelin]

Ok