feat(ring_theory/multiplicity): multiplicity of elements of a ring #523
Conversation
| @@ -859,4 +859,5 @@ lemma with_bot.add_eq_one_iff : ∀ {n m : with_bot ℕ}, n + m = 1 ↔ (n = 0 | |||
| | (some n) (some (m + 1)) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe, | |||
| with_bot.coe_eq_coe, with_bot.coe_eq_coe]; simp [nat.add_succ, nat.succ_inj', nat.succ_ne_zero] | |||
|
|
|||
|
|
|||
There was a problem hiding this comment.
Double empty line
| @@ -954,6 +954,10 @@ lemma num_ne_zero_of_ne_zero {q : ℚ} (h : q ≠ 0) : q.num ≠ 0 := | |||
| assume : q.num = 0, | |||
| h $ zero_of_num_zero this | |||
|
|
|||
| @[simp] lemma num_one : (1 : ℚ).num = 1 := rfl | |||
There was a problem hiding this comment.
Should these two simp-lemmas be generalised to arbitrary integers?
There was a problem hiding this comment.
That's not so much a generalization as a different lemma
There was a problem hiding this comment.
Aah, of course. So, let's leave it like this.
ring_theory/multiplicity.lean
Outdated
| nat.cases_on k (λ _, one_dvd _) | ||
| (λ k ⟨h₁, h₂⟩, by_contradiction (λ hk, (nat.find_min _ (lt_of_succ_le (h₂ ⟨k, hk⟩)) hk))) | ||
|
|
||
| lemma spec {a b : α} (h : finite a b) : a ^ get (multiplicity a b) h ∣ b := |
There was a problem hiding this comment.
Should this be called something like pow_multiplicity_dvd?
| open multiplicity | ||
|
|
||
| lemma multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1) | ||
| (hle : multiplicity p a ≤ multiplicity p b) |
There was a problem hiding this comment.
Is this the natural condition to put here? I would think that p \dvd b would be more natural...
There was a problem hiding this comment.
I guess it's natural, but not trivially equivalent, and actually this is a harder lemma to prove than the version with p \dvd b.
This statement is copied from padic_val. I guess Rob had a use for it in this form.
There was a problem hiding this comment.
So maybe we should provide both?
There was a problem hiding this comment.
The p \| b version is fairly trivial to prove, and fairly niche, so I wouldn't bother with it.
|
LGTM |
#495 extends this PR. This PR adds multiplicity without removing
padic_val.TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list