lint

Stream: new members

[vxctyxeha]

Why is there a #lint issue? I have already assumed that p is a prime number.

import Mathlib
lemma  Gp{G : Type*} [CommGroup G] [Fintype G][Fact (Nat.Prime p)]
  (_: p ∣ Fintype.card G) :(1 : G) ∈ {g : G | ∃ k : ℕ, orderOf g = p ^ k} := by
  change (∃ k : ℕ, orderOf (1 : G) = p ^ k)
  rw [orderOf_one]
  use 0
  rw [pow_zero p]
#lint

[Aaron Liu]

The don't need the fact the p is prime, or the fact that G is finite, or the fact that p divides the order of G.

[vxctyxeha]

屏幕截图 2025-05-17 012547.png
but the definition is said to be prime

[Aaron Liu]

Well evidently it works when it's not prime too

[vxctyxeha]

looks like there is a def https://github.com/leanprover-community/mathlib4/blob/52e9c62bb1c948ac7d8c8c23f21ef9fa7e775c41/Mathlib/GroupTheory/PGroup.lean#L36-L37

[vxctyxeha]

But the two definitions are not equivalent.