exists_one_add_mul_pow_prime_eq — Mathlib

English

Let R be a commutative semiring, p a prime, and u, v in R with v | u and puv | u^p. Then for every x in R there exists y in R such that (1 + u x)^p = 1 + p u (x + v y).

Русский

Пусть R — коммутативное полускольное кольцо, p — простое число, и элементы u, v в R удовлетворяют v | u и p u v | u^p. Тогда для каждого x ∈ R существует y ∈ R such that (1 + u x)^p = 1 + p u (x + v y).

LaTeX

$$$\\\\forall R [CommSemiring R], \\\\forall u, v \\\\in R, \\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\\\wedge v \\\\\\mid u \\\\wedge p u v \\\\\\mid u^{p} \\\\Rightarrow \\\\forall x \\\\in R, \\\\exists y \\\\in R, (1 + u x)^{p} = 1 + p u (x + v y).$$$$

Lean4

theorem exists_one_add_mul_pow_prime_eq (hp : p.Prime) (hvu : v ∣ u) (hpuv : p * u * v ∣ u ^ p) (x : R) :
    ∃ y, (1 + u * x) ^ p = 1 + p * u * (x + v * y) :=
  by
  rw [add_comm, add_pow]
  rw [← Finset.add_sum_erase (a := 0) _ _ (by simp)]
  simp_rw [one_pow, pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one]
  rw [← Finset.add_sum_erase (a := 1) _ _ (by simp [hp.pos])]
  rw [←
    Finset.sum_erase_add (a := p) _ _
      (by -- aesop works but is slow

        simp only [Finset.mem_erase]
        rw [← and_assoc, and_comm (a := ¬_), ← Nat.two_le_iff]
        simp [hp.two_le])]
  obtain ⟨a, ha⟩ := hvu
  obtain ⟨b, hb⟩ := hpuv
  use
    a * x ^ 2 * ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (p.choose i / p : ℕ) +
      b * x ^ p
  rw [mul_add]
  congr 2
  · rw [Nat.choose_one_right]; ring
  simp only [mul_add, Finset.mul_sum]
  congr 1
  · congr! 1 with i hi
    simp only [Finset.mem_erase, ne_eq, Finset.mem_range] at hi
    have hi' : 2 ≤ i := by omega
    calc
      (u * x) ^ i * p.choose i = (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by cutsat)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by rw [ha]; ring
  ·
    calc
      (u * x) ^ p * (p.choose p) = u ^ p * x ^ p := by simp [Nat.choose_self, mul_pow]
      _ = p * u * v * b * x ^ p := by rw [hb]
      _ = p * u * (v * (b * x ^ p)) := by ring_nf

Похожие утверждения