proofs/math/natural/lcm.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as Lcm

7 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R
import ./gcd.bend as G

Definitions

def add_succ_zero source · line 16 · raw

@+b:Nat -> @+x:Nat -> @+e:{Nat.add(b, 1n+x) == 0n : Nat} -> Empty

def one_s source · line 19 · raw

@+ap:Nat -> @+bq:Nat -> @+e:{Nat.add(bq, Nat.mul(ap, 1n+bq)) == 0n : Nat} -> {1n+ap == 1n : Nat}

def mul_eq_one source · line 27 · raw

@+a:Nat -> @+b:Nat -> @+e:{Nat.mul(a, b) == 1n : Nat} -> {a == 1n : Nat}

a b == 1 gives a == 1 (Mathlib Nat.eq_one_of_mul_eq_one_right)

def one_mul source · line 36 · raw

@+d:Nat -> {Nat.mul(1n, d) == d : Nat}

def dvd_antisymm source · line 40 · raw

@+x:Nat -> @+y:Nat -> @+kx:Nat -> @+ky:Nat -> @+ex:{x == Nat.mul(kx, y) : Nat} -> @+ey:{y == Nat.mul(ky, x) : Nat} -> {x == y : Nat}

x == kx y and y == ky x give x == y (Mathlib Nat.dvd_antisymm)

def swap_cw source · line 54 · raw

@+c:Nat -> @+w:Nat -> @+g:Nat -> {Nat.mul(c, Nat.mul(w, g)) == Nat.mul(w, Nat.mul(c, g)) : Nat}

c (w g) == w (c g)

def scale_dvd source · line 62 · raw

@+c:Nat -> @+x:Nat -> @+w:Nat -> @+g:Nat -> @+e:{x == Nat.mul(w, g) : Nat} -> {Nat.mul(c, x) == Nat.mul(w, Nat.mul(c, g)) : Nat}

x == w g gives c x == w (c g)

def unscale source · line 66 · raw

@+cp:Nat -> @+x:Nat -> @+w:Nat -> @+h:Nat -> @+e:{Nat.mul(1n+cp, x) == Nat.mul(w, Nat.mul(h, 1n+cp)) : Nat} -> {x == Nat.mul(w, h) : Nat}

c x == w (h c) gives x == w h (c > 0)

def gcd_mul_pos source · line 69 · raw

@+cp:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(Nat.mul(1n+cp, a), Nat.mul(1n+cp, b)) == Nat.mul(1n+cp, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b)) : Nat}

def gcd_mul_left source · line 95 · raw

@+c:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(Nat.mul(c, a), Nat.mul(c, b)) == Nat.mul(c, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b)) : Nat}

gcd(c a, c b) == c gcd(a, b) (Mathlib Nat.gcd_mul_left)

def gcd_pos source · line 105 · raw

@+ap:Nat -> @+l:Nat -> @+g:Nat -> @+e:{1n+ap == Nat.mul(l, g) : Nat} -> {Nat.is_lt(0n, g) == True{} : Bool}

a == la g with a > 0 makes g positive

def div_exact source · line 112 · raw

@+x:Nat -> @+l:Nat -> @+g:Nat -> @+hg:{Nat.is_lt(0n, g) == True{} : Bool} -> @+e:{x == Nat.mul(l, g) : Nat} -> {Nat.div(x, g) == l : Nat}

def lcm_pos source · line 120 · raw

@+ap:Nat -> @+bp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(1n+ap, 1n+bp) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/gcd.wl(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/natural/gcd.ws(1n+bp, 1n+ap, 1n+bp)), 1n+bp) : Nat}

def lcm_wl source · line 127 · raw

@+a:Nat -> @+b:Nat -> Nat

lcm(a, b) == kl a and lcm(a, b) == kr b (Mathlib Nat.dvd_lcm_left/right)

def lcm_wr source · line 136 · raw

@+a:Nat -> @+b:Nat -> Nat

def dvd_lcm_left source · line 145 · raw

@+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(a, b) == Nat.mul(lcm_wl(a, b), a) : Nat}

def dvd_lcm_right source · line 160 · raw

@+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(a, b) == Nat.mul(lcm_wr(a, b), b) : Nat}

def gcd_mul_lcm source · line 170 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(a, b)) == Nat.mul(a, b) : Nat}

gcd(a, b) lcm(a, b) == a b (Mathlib Nat.gcd_mul_lcm)

def cancel_pos source · line 184 · raw

@+x:Nat -> @+y:Nat -> @+g:Nat -> @+hg:{Nat.is_lt(0n, g) == True{} : Bool} -> @+e:{Nat.mul(x, g) == Nat.mul(y, g) : Nat} -> {x == y : Nat}

def lcm_dw source · line 192 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> Nat

the quotient m / lcm(a, b) for a common multiple m == x a == y b

def lcm_dvd_pos source · line 201 · raw

@+ap:Nat -> @+bp:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> @+ex:{m == Nat.mul(x, 1n+ap) : Nat} -> @+ey:{m == Nat.mul(y, 1n+bp) : Nat} -> {m == Nat.mul(lcm_dw(1n+ap, 1n+bp, m, x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(1n+ap, 1n+bp)) : Nat}

def lcm_dvd source · line 222 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> @+ex:{m == Nat.mul(x, a) : Nat} -> @+ey:{m == Nat.mul(y, b) : Nat} -> {m == Nat.mul(lcm_dw(a, b, m, x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(a, b)) : Nat}

every common multiple of a and b is a multiple of lcm(a, b) (Mathlib Nat.lcm_dvd)