Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/goal.lean

Created August 8, 2018 12:41
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/f515877383946b5eb84f03e31cb988c3 to your computer and use it in GitHub Desktop.
Save kbuzzard/f515877383946b5eb84f03e31cb988c3 to your computer and use it in GitHub Desktop.
Download ZIP
goal
Raw
goal.lean
| @finset.sum.{0 0} nat
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@semiring.to_add_comm_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@ring.to_semiring.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.ring.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(finset.range (@has_add.add.{0} nat nat.has_add k (@has_one.one.{0} nat nat.has_one)))
(λ (i : nat),
@has_mul.mul.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.has_mul.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@has_pow.pow.{0 0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
nat
(@monoid.has_pow.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@ring.to_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.ring.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(@mv_polynomial.C.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))
(@coe.{1 1} nat rat
(@coe_to_lift.{1 1} nat rat
(@coe_base.{1 1} nat rat
(@nat.cast_coe.{0} rat
(@mul_zero_class.to_has_zero.{0} rat
(@semiring.to_mul_zero_class.{0} rat
(@ring.to_semiring.{0} rat
(@comm_ring.to_ring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))))
(@monoid.to_has_one.{0} rat
(@ring.to_monoid.{0} rat
(@comm_ring.to_ring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(@distrib.to_has_add.{0} rat
(@ring.to_distrib.{0} rat
(@comm_ring.to_ring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))))))
(@nat.Prime.p _inst_1)))
i)
(@has_pow.pow.{0 0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
nat
(@monoid.has_pow.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@ring.to_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.ring.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(@mv_polynomial.X.{0 0} rat nat nat.decidable_eq rat.decidable_eq
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))
i)
(@has_pow.pow.{0 0} nat nat nat.has_pow (@nat.Prime.p _inst_1) (@has_sub.sub.{0} nat nat.has_sub k i))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment