EuclideanDomain.gcd

Stream: new members

[tsuki]

In EuclideanDomain.gcd, what is the corresponding lemma for the deduction that a|gcd(m,n) and gcd(m,n)|a leads to a=gcd(m,n)? I mean how to prove the theorem using h2 and h3?

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

theorem gcd_demo (n : ℝ) (h₀ : 0 < n) : EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) = 1 := by
  have h₁: (196/883) * (11 * n^2 + 4) + (33/883-154*n/883)*(14 * n + 3) = 1 := by
    ring
  have h₂: 1 ∣ EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) := by
    exact one_dvd (EuclideanDomain.gcd (11 * n ^ 2 + 4) (14 * n + 3))
  have h₃:  EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) ∣ (196/883) * (11 * n^2 + 4) + (33/883-154*n/883)*(14 * n + 3) := by
    have t₁: EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) ∣ (11 * n^2 + 4) := by
      exact EuclideanDomain.gcd_dvd_left (11 * n ^ 2 + 4) (14 * n + 3)
    have t₂: EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) ∣ (14 * n + 3) := by
      exact EuclideanDomain.gcd_dvd_right (11 * n ^ 2 + 4) (14 * n + 3)
    exact Dvd.dvd.linear_comb t₁ t₂ (196 / 883) (33 / 883 - 154 * n / 883)
  rw[h₁] at h₃
  sorry

[Ruben Van de Velde]

It's docs#dvd_antisymm , but it's not true for real numbers

[Ruben Van de Velde]

In particular because any two non-zero reals divide each other

[tsuki]

I have tried the tactic,it seems not to work.

[Aaron Liu]

The reals are a euclidean domain in a trivial way

[Aaron Liu]

And every nonzero element is a unit

[Aaron Liu]

The best you'll get is that they're docs#Associated

[Aaron Liu]

And that just means they're both zero or both nonzero

[Aaron Liu]

docs#associated_of_dvd_dvd

[Luigi Massacci]

I assume the n : \R was meant to be n : \N or n : \Z

[Ruben Van de Velde]

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

lemma Field.mod {K : Type*} [Field K] [DecidableEq K] (a b : K) : a % b = a - a * b / b := rfl

lemma Field.gcd {K : Type*} [Field K] [DecidableEq K] (a b : K) : EuclideanDomain.gcd a b = if a = 0 then b else a := by
  unfold EuclideanDomain.gcd
  split_ifs <;> simp [*, mod]

theorem gcd_demo (n : ℝ) (h₀ : 0 < n) : EuclideanDomain.gcd (11 * n^2 + 4) (14 * n + 3) = 1 := by
  rw [← sub_eq_zero, Field.gcd]
  split_ifs
  · have : 0 < 14 * n + 3 - 1 := by rw [add_sub_assoc]; norm_num; positivity
    simp [this.ne']
    sorry
  · have : 0 < 11 * n^2 + 4 - 1 := by rw [add_sub_assoc]; norm_num; positivity
    simp [this.ne']
    sorry

[tsuki]

I think the issue really lies in x : ℝ. Actually, I want to represent the gcd of two polynomials. How should I write (11 * n^2 + 4) to ensure its type is a polynomial?*

[Ruben Van de Velde]

With docs#Polynomial :)

[Ruben Van de Velde]

I wrote #23334 with those lemmas