English
Compatibility of a lifted binary operation on rationals with the corresponding integer operations; under appropriate nondegeneracy conditions, the lifted operation agrees with the rational division representation.
Русский
Совместимость поднимаемой бинарной операции на рациональных числах с соответствующими целочисленными операциями; при соответствующих условиях согласуется с представлением через деление.
LaTeX
$$$ \text{lift_binop_eq}\; (f)\; (f_1)\; (f_2) \; (fv) \; (f_0) \; (a,b,c,d) \; (b_0,d_0) \; (H) \Rightarrow f(\text{Rat.divInt } a b)(\text{Rat.divInt } c d) = \text{Rat.divInt}(f_1 a b c d)(f_2 a b c d) $$$
Lean4
theorem lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
(fv : ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂}, f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = f₁ n₁ d₁ n₂ d₂ /. f₂ n₁ d₁ n₂ d₂)
(f0 : ∀ {n₁ d₁ n₂ d₂}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0) (a b c d : ℤ) (b0 : b ≠ 0) (d0 : d ≠ 0)
(H :
∀ {n₁ d₁ n₂ d₂}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d :=
by
generalize ha : a /. b = x; obtain ⟨n₁, d₁, h₁, c₁⟩ := x; rw [mk'_eq_divInt] at ha
generalize hc : c /. d = x; obtain ⟨n₂, d₂, h₂, c₂⟩ := x; rw [mk'_eq_divInt] at hc
rw [fv]
have d₁0 := Int.ofNat_ne_zero.2 h₁
have d₂0 := Int.ofNat_ne_zero.2 h₂
exact
(divInt_eq_divInt_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
(H ((divInt_eq_divInt_iff b0 d₁0).1 ha) ((divInt_eq_divInt_iff d0 d₂0).1 hc))
