Algebra.GroupPower.Order

Stream: mathlib4

[Siddhartha Gadgil]

I have started porting Algebra.GroupPower.Order, and everything is ported except for a theorem pow_bit0_pos_iff which depends on an unported result in Lean core, as everything to do with bit0 seems deprecated.

I was going to ask if this should be commented out, but I see that this has an important corollary: theorem sq_pos_iff (a : R) : 0 < a ^ 2 ↔ a ≠ 0.
What would be a good policy:

• port the results on bit0
• port a modification using doubles and prove only the result about squares and the lemmas along the way.

I feel the second has the advantage that if the deprecated bit0 is removed we can have the other results still.

[Yaël Dillies]

The bit0 and bit1 lemmas have (/had?) the avantage that they apply to numerals.

[Siddhartha Gadgil]

Do you think they are worth porting then (at least the ones that are used)?

[Yaël Dillies]

I don't know how numerals work in Lean 4, but if there is a way of seeing whether a numeral is even or odd from the head symbol, yes definitely.

[Floris van Doorn]

No, the head symbol of numerals is not bit0/bit1 anymore, so I expect that simp and rw will not be able to deal well with lemmas about bit0 and bit1 anymore.

[Kevin Buzzard]

This is really a result about even and odd -- the fact that in lean 3 we chose to express them via bit0 is now a historical coincidence. Are we in a position to port data.nat.parity? If not then we could make data.nat.parity.defs and that would be a nice way forward

[Floris van Doorn]

We can still state lemmas about bit0/bit1, but I don't know if that will be nicer than 2 * _ or 2 * _ + 1. I think both forms will not easily match the numerals 16 or 17 (but I might be wrong, I didn't check).

[Siddhartha Gadgil]

As they are marked as deprecated, a file with lemmas about them is rejected.

[Siddhartha Gadgil]

I should also add that the PR is mathlib4#1043 and given my timezone if anyone wants to take over they are welcome.

[Yaël Dillies]

Kevin Buzzard said:

This is really a result about even and odd -- the fact that in lean 3 we chose to express them via bit0 is now a historical coincidence. Are we in a position to port data.nat.parity? If not then we could make data.nat.parity.defs and that would be a nice way forward

It's not a historical coincidence at all. I made sure that all lemmas were available in both spellings.

[Ruben Van de Velde]

Please port the bit lemmas, even though they won't apply directly to numerals. You'll need a set_option - see all other declarations about bit in the tree for examples

[Yaël Dillies]

Also, Kevin, why data.nat.parity? Everything is in file#algebra/parity which is very low import now.

[Kevin Buzzard]

Yael I'm sure you know a lot more about parity than me :-)

[Siddhartha Gadgil]

Sure. I will port the bit lemmas

[Siddhartha Gadgil]

Actually some of this has been ported either for Positivity or Linarithmetic. I will deduplicated and clean up.

[Siddhartha Gadgil]

Just to confirm mathlib4#1043 is ready for review