Zulip Chat Archive

Stream: mathlib4

Topic: !4#3761 LinearAlgebra.Matrix.Zpow

Moritz Firsching (Apr 27 2023 at 12:32):

In LinearAlgebra.Matrix.Zpow, should it be ZPow instead of Zpow?
There is already Mathlib.GroupTheory.Subgroup.Zpowers, so if we aim for consistency we might want to change both?!

Jeremy Tan (Apr 27 2023 at 12:33):

We already have ZMod, so we should use ZPow

Jeremy Tan (Apr 27 2023 at 12:33):

I'm 100% for ZPow

Moritz Firsching (Apr 27 2023 at 12:34):

ok, also Mathlib.GroupTheory.Subgroup.ZPowers?

Jeremy Tan (Apr 27 2023 at 12:36):

LinearAlgebra.Matrix.ZPow, and Mathlib.GroupTheory.Subgroup.ZPowers, but do the latter in another PR

Eric Wieser (Apr 27 2023 at 12:36):

Let's wait for a few more opinions, but I agree with the consistency argument with ZMod

Jeremy Tan (Apr 27 2023 at 12:36):

just as the capitalisation of zmod is ZMod, kinda like IJsselmeer

Last updated: Dec 20 2023 at 11:08 UTC