gammaSet_div_gcd_to_gammaSet10_bijection

English

If v ∈ gammaSet(1,r,0), then v = r • (divIntMap r v).

Русский

Если $v \in \gammaSet(1,r,0)$, то $v = r \cdot (\mathrm{divIntMap}\ r\ v)$.

LaTeX

$$$v = r \cdot (\mathrm{divIntMap}\ r\ v).$$$

Lean4

theorem gammaSet_div_gcd_to_gammaSet10_bijection (r : ℕ) [NeZero r] :
    Set.BijOn (divIntMap r) (gammaSet 1 r 0) (gammaSet 1 1 0) :=
  by
  refine ⟨?_, ?_, ?_⟩
  · intro x hx
    simp only [divIntMap, mem_gammaSet_one] at *
    exact finGcdMap_div _ hx.2
  · intro x hx v hv hv2
    ext i
    exact (Int.ediv_left_inj (gammaSet_div_gcd hx i) (gammaSet_div_gcd hv i)).mp (congr_fun hv2 i)
  · intro x hx
    use r • x
    simp only [nsmul_eq_mul, divIntMap, Int.cast_natCast]
    constructor
    · rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
      exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩
    · ext i
      simp_all [NeZero.ne r]

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