leanprover-community / mathlib

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

Zulip Chat Archive

Stream: maths

Topic: has_pow for fpow


Chris Hughes (Nov 03 2018 at 12:42):

There's no has_pow instance for integer powers in a field, there's just fpow. Is there a reason why the notation isn't used for fpow?

Mario Carneiro (Nov 03 2018 at 13:28):

maybe it was written before has_pow? I think @Rob Lewis will know


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll