Parity lemmas for natural numbers

Stream: maths

[Michael Stoll]

In #16290, I introduce a few lemmas

lemma odd.mod_even_iff {n a : ℕ} (ha : even a) : odd n ↔ odd (n % a)
lemma even.mod_even_iff {n a : ℕ} (ha : even a) : even n ↔ even (n % a)
lemma odd.mod_even {n a : ℕ} (hn : odd n) (ha : even a) : odd (n % a)
lemma even.mod_even {n a : ℕ} (hn : even n) (ha : even a) : even (n % a)
lemma odd.factors_ne_two {n p : ℕ} (hn : odd n) (hp : p ∈ n.factors) : p ≠ 2

(in part based on suggestions by @Junyan Xu).
Question: Should they full name be nat.odd.... or just odd....?
The first seems more appropriate in view of the statements, but the second is more convenient for dot notation.
Opinions?

[Yaël Dillies]

The first two should be reversed.

[Michael Stoll]

The first is about odd ↔ odd, the second about even ↔ even, and in both we go mod an even number. So I think the names are OK (but for the first two, dot notation is maybe less relevant).

[Michael Stoll]

Or did you mean the statements, not the names?

[Floris van Doorn]

the iffs

[Michael Stoll]

Because the RHS looks more complicated?

[Floris van Doorn]

Yes, so it should become the LHS.

[Michael Stoll]

OK.

[Kevin Buzzard]

iff is not symmetric in Lean! Tactics like rw and simp change the LHS to the RHS, so the rule is to always have the LHS the less simple of the two sides.

[Michael Stoll]

In my use case, I need the other direction (i.e., odd.mod_even), but I see the point.

[Michael Stoll]

But this discussion does not answer my original question.