theorem
nat.find_le
{p q : ℕ → Prop}
[decidable_pred p]
[decidable_pred q]
(h : ∀ (n : ℕ), q n → p n)
(hp : ∃ (n : ℕ), p n)
(hq : ∃ (n : ℕ), q n) :
multiplicity a b returns the largest natural number n such that
a ^ n ∣ b, as an enat or natural with infinity. If ∀ n, a ^ n ∣ b,
then it returns ⊤
theorem
multiplicity.finite_iff_dom
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity.finite a b ↔ (multiplicity a b).dom
theorem
multiplicity.not_unit_of_finite
{α : Type u_1}
[comm_monoid α]
{a b : α}
(h : multiplicity.finite a b) :
theorem
multiplicity.finite_of_finite_mul_left
{α : Type u_1}
[comm_monoid α]
{a b c : α}
(a_1 : multiplicity.finite a (b * c)) :
theorem
multiplicity.finite_of_finite_mul_right
{α : Type u_1}
[comm_monoid α]
{a b c : α}
(a_1 : multiplicity.finite a (b * c)) :
theorem
multiplicity.pow_dvd_of_le_multiplicity
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(a_1 : ↑k ≤ multiplicity a b) :
theorem
multiplicity.pow_multiplicity_dvd
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
(h : multiplicity.finite a b) :
a ^ (multiplicity a b).get h ∣ b
theorem
multiplicity.is_greatest
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{m : ℕ}
(hm : multiplicity a b < ↑m) :
theorem
multiplicity.is_greatest'
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{m : ℕ}
(h : multiplicity.finite a b)
(hm : (multiplicity a b).get h < m) :
theorem
multiplicity.unique
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(hk : a ^ k ∣ b)
(hsucc : ¬a ^ (k + 1) ∣ b) :
↑k = multiplicity a b
theorem
multiplicity.unique'
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(hk : a ^ k ∣ b)
(hsucc : ¬a ^ (k + 1) ∣ b) :
k = (multiplicity a b).get _
theorem
multiplicity.le_multiplicity_of_pow_dvd
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(hk : a ^ k ∣ b) :
↑k ≤ multiplicity a b
theorem
multiplicity.pow_dvd_iff_le_multiplicity
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ} :
theorem
multiplicity.multiplicity_lt_iff_neg_dvd
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ} :
theorem
multiplicity.eq_some_iff
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{n : ℕ} :
theorem
multiplicity.eq_top_iff
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
theorem
multiplicity.one_right
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : ¬is_unit a) :
multiplicity a 1 = 0
@[simp]
theorem
multiplicity.get_one_right
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : multiplicity.finite a 1) :
(multiplicity a 1).get ha = 0
@[simp]
theorem
multiplicity.multiplicity_unit
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(b : α)
(ha : is_unit a) :
multiplicity a b = ⊤
@[simp]
theorem
multiplicity.one_left
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
(b : α) :
multiplicity 1 b = ⊤
theorem
multiplicity.multiplicity_eq_zero_of_not_dvd
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
(ha : ¬a ∣ b) :
multiplicity a b = 0
theorem
multiplicity.eq_top_iff_not_finite
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b = ⊤ ↔ ¬multiplicity.finite a b
theorem
multiplicity.multiplicity_le_multiplicity_iff
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b c d : α} :
multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
theorem
multiplicity.dvd_of_multiplicity_pos
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
(h : 0 < multiplicity a b) :
a ∣ b
theorem
multiplicity.dvd_iff_multiplicity_pos
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
0 < multiplicity a b ↔ a ∣ b
@[instance]
Equations
- multiplicity.decidable_nat = λ (a b : ℕ), decidable_of_iff (a ≠ 1 ∧ 0 < b) _
@[instance]
Equations
- multiplicity.decidable_int = λ (a b : ℤ), decidable_of_iff (a.nat_abs ≠ 1 ∧ b ≠ 0) _
theorem
multiplicity.ne_zero_of_finite
{α : Type u_1}
[comm_monoid_with_zero α]
{a b : α}
(h : multiplicity.finite a b) :
b ≠ 0
@[simp]
theorem
multiplicity.zero
{α : Type u_1}
[comm_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
(a : α) :
multiplicity a 0 = ⊤
theorem
multiplicity.min_le_multiplicity_add
{α : Type u_1}
[comm_semiring α]
[decidable_rel has_dvd.dvd]
{p a b : α} :
min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
@[simp]
theorem
multiplicity.neg
{α : Type u_1}
[comm_ring α]
[decidable_rel has_dvd.dvd]
(a b : α) :
multiplicity a (-b) = multiplicity a b
theorem
multiplicity.multiplicity_add_of_gt
{α : Type u_1}
[comm_ring α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(h : multiplicity p b < multiplicity p a) :
multiplicity p (a + b) = multiplicity p b
theorem
multiplicity.multiplicity_sub_of_gt
{α : Type u_1}
[comm_ring α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(h : multiplicity p b < multiplicity p a) :
multiplicity p (a - b) = multiplicity p b
theorem
multiplicity.multiplicity_add_eq_min
{α : Type u_1}
[comm_ring α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(h : multiplicity p a ≠ multiplicity p b) :
multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
theorem
multiplicity.finite_mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{p a b : α}
(hp : prime p)
(a_1 : multiplicity.finite p a)
(a_2 : multiplicity.finite p b) :
multiplicity.finite p (a * b)
theorem
multiplicity.finite_mul_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{p a b : α}
(hp : prime p) :
multiplicity.finite p (a * b) ↔ multiplicity.finite p a ∧ multiplicity.finite p b
theorem
multiplicity.finite_pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{p a : α}
(hp : prime p)
{k : ℕ}
(ha : multiplicity.finite p a) :
multiplicity.finite p (a ^ k)
@[simp]
theorem
multiplicity.multiplicity_self
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : ¬is_unit a)
(ha0 : a ≠ 0) :
multiplicity a a = 1
@[simp]
theorem
multiplicity.get_multiplicity_self
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : multiplicity.finite a a) :
(multiplicity a a).get ha = 1
theorem
multiplicity.mul'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(hp : prime p)
(h : (multiplicity p (a * b)).dom) :
(multiplicity p (a * b)).get h = (multiplicity p a).get _ + (multiplicity p b).get _
theorem
multiplicity.mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(hp : prime p) :
multiplicity p (a * b) = multiplicity p a + multiplicity p b
theorem
multiplicity.finset.prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{β : Type u_2}
{p : α}
(hp : prime p)
(s : finset β)
(f : β → α) :
multiplicity p (∏ (x : β) in s, f x) = ∑ (x : β) in s, multiplicity p (f x)
theorem
multiplicity.pow'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p a : α}
(hp : prime p)
(ha : multiplicity.finite p a)
{k : ℕ} :
(multiplicity p (a ^ k)).get _ = k * (multiplicity p a).get ha
theorem
multiplicity.pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p a : α}
(hp : prime p)
{k : ℕ} :
multiplicity p (a ^ k) = k •ℕ multiplicity p a
theorem
multiplicity.multiplicity_pow_self
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p : α}
(h0 : p ≠ 0)
(hu : ¬is_unit p)
(n : ℕ) :
multiplicity p (p ^ n) = ↑n
theorem
multiplicity.multiplicity_pow_self_of_prime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p : α}
(hp : prime p)
(n : ℕ) :
multiplicity p (p ^ n) = ↑n
theorem
multiplicity_eq_zero_of_coprime
{p a b : ℕ}
(hp : p ≠ 1)
(hle : multiplicity p a ≤ multiplicity p b)
(hab : a.coprime b) :
multiplicity p a = 0