Zulip Chat Archive

Stream: general

Topic: fpow and gpow

Sebastien Gouezel (Oct 26 2021 at 14:26):

For int powers, we use currently gpow and fpow. I guess gpow is for "group power" and fpow is for "field power"? Since we have groups with zeroes, the boundary between the two is not clear at all. Here is a random proof on fpow:

lemma fpow_nonneg {a : K} (ha : 0 ≤ a) : ∀ (z : ℤ), 0 ≤ a ^ z
| (n : ℕ) := by { rw gpow_coe_nat, exact pow_nonneg ha _ }
| -[1+n]  := by { rw gpow_neg_succ_of_nat, exact inv_nonneg.2 (pow_nonneg ha _) }

Yes, the proof uses gpow lemmas all over the place. And when I try to find a lemma, half of the time it is an fpow and half of the time it is a gpow, so automatic completion doesn't work well. What would you think of a serious clean-up, using zpow everywhere?

Yury G. Kudryashov (Oct 26 2021 at 14:29):

Having gpow and fpow made sense some time ago when they used separate definitions etc. I think that it makes much less sense now but there are situations when fpow lemmas need more assumptions. E.g., compare docs#fpow_add and docs#gpow_add.

Yury G. Kudryashov (Oct 26 2021 at 14:29):

What do you suggest for these lemmas?

Sebastien Gouezel (Oct 26 2021 at 14:42):

We could have zpow_add for the first one, and when there is a special version for groups we could spell it gzpow_add. The point being that most lemmas wouldn't have the g, and that this would not break tab completion.

Johan Commelin (Oct 26 2021 at 14:44):

How about appending a ₀ for lemmas about groups with zero? That's what we've started doing elsewhere in the library.

Sebastien Gouezel (Oct 26 2021 at 14:45):

Many lemmas are true in general div_inv_monoids.

Yaël Dillies (Oct 26 2021 at 14:46):

Was about to bring up ₀. This is the way forward.

Yaël Dillies (Oct 26 2021 at 14:48):

For other cases, like truncated subtraction vs add_group subtraction, set lattice operations vs lattice operations, we changed the actual name of the operation, but I don't think there's a need for that here.

Johan Commelin (Oct 26 2021 at 14:50):

So for Yury's example I would suggest gpow_add → zpow_add and fpow_add → zpow_add₀.

Sebastien Gouezel (Oct 26 2021 at 14:52):

With the zero used in general div_inv_monoids, and only when disambiguation is needed? I think I like that.

Reid Barton (Oct 26 2021 at 15:00):

While we're at it, can we also rename gsmul to zsmul for parallelism with nsmul?

Sebastien Gouezel (Oct 26 2021 at 15:07):

Maybe in two separate PRs. This one will be painful enough :-)

Yakov Pechersky (Oct 26 2021 at 16:15):

Anne asked if there is some sort of general cancellative_inv_monoid where fpow makes sense. I tried to code it up but ran into issues, as part of giving matrices an fpow:
https://github.com/leanprover-community/mathlib/pull/8683#issuecomment-922407544

Eric Wieser (Oct 26 2021 at 18:10):

On a related note; I was also wondering whether we want to make ring.inverse a field of ring so that we can just use \inv on rings. In particular, it would be nice to unify docs#matrix.has_inv and docs#ring.inverse such that ring.inverse A.det • A.adjugate = ring.inverse A was true by definition

Reid Barton (Oct 26 2021 at 20:20):

As in an actual field of the ring structure? I'm not a big fan because ring.inverse is nonalgebraic (e.g. it's not preserved by ring homomorphisms or computed componentwise in product instances)

Sebastien Gouezel (Oct 26 2021 at 20:52):

#9989 (wow, 10000 is getting pretty close!)

Yaël Dillies (Oct 26 2021 at 20:53):

Yes!! Who will be the lucky one?

Yaël Dillies (Oct 26 2021 at 20:53):

Can you believe that we were at 6500 when I joined?

Kevin Buzzard (Oct 26 2021 at 21:02):

Can you believe that we were at 21 when I joined??

Kevin Buzzard (Oct 26 2021 at 21:02):

What's happened here over the last four years is really quite extraordinary

Thomas Browning (Oct 26 2021 at 21:06):

Anyone got a good PR lined up for #10000 ?

Yaël Dillies (Oct 26 2021 at 21:14):

I can make it Szemerédi regularity lemma, but it will wait for quite a while before being merged. Also, I don't want to spoil anyone else's opportunity on this one.