leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: power


Ashvni Narayanan (Jun 30 2020 at 23:20):

I have a field K, and an element x : K. I want to define x^n for n:\Z. But this gives me an error. There is no problem with n:\N.
Is there a way I can resolve it? Any help is appreciated. Thank you!

Bryan Gin-ge Chen (Jun 30 2020 at 23:21):

import algebra.field_power should work.

Ashvni Narayanan (Jun 30 2020 at 23:22):

Yes, that works. Thank you!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll