Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/long goal

Last active June 18, 2019 08:28
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kbuzzard/33fe4da55bcc83199306c133f6c4d865 to your computer and use it in GitHub Desktop.
Save kbuzzard/33fe4da55bcc83199306c133f6c4d865 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
long goal
1 goal
p : nat,
n : nat
⊢ @eq.{1}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@has_mul.mul.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@ideal.quotient.has_mul.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@has_zero.zero.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@mul_zero_class.to_has_zero.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@semiring.to_mul_zero_class.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@ring.to_semiring.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@comm_ring.to_ring.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@ideal.quotient.comm_ring.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n
(@has_one.one.{0} nat nat.has_one)))))))))))))
(@ideal.quotient.mk.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)))))))
(@has_pow.pow.{0 0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
nat
(@monoid.has_pow.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@ring.to_monoid.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), (λ (a b : int), int.decidable_eq a b) a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.X.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), (λ (a b : int), int.decidable_eq a b) a b)
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_sub.sub.{0} nat nat.has_sub
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)))))))
(@has_zero.zero.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@add_monoid.to_has_zero.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@dah.{0}
(@ideal.quotient.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_emptyc.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@set.has_insert.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
(@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@coe.{1 1} nat int
(@coe_to_lift.{1 1} nat int
(@coe_base.{1 1} nat int
(@nat.cast_coe.{0} int
(@mul_zero_class.to_has_zero.{0} int
(@semiring.to_mul_zero_class.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@monoid.to_has_one.{0} int
(@semiring.to_monoid.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))
(@distrib.to_has_add.{0} int
(@semiring.to_distrib.{0} int
(@comm_semiring.to_semiring.{0} int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))
(@has_pow.pow.{0 0} nat nat nat.has_pow p
(@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
(@ideal.quotient.comm_ring.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@ideal.span.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : int), int.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
(@singleton.{0 0}
(@mv_polynomial.{0 0} nat int
(@nonzero_comm_semiring.to_comm_semiring.{0} int
(@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
(@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
(set.{0}
(@mv_polynomial.{0 0} nat int
(@comm_ring.to_comm_semiring.{0} int (@nonzero_comm_ring.to_comm_ring.{0} int …))))
…
…
…))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment