michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/int/div): int div

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-09 15:04:01 -07:00
parent 1ffe62341b
commit a23c05549e
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/int/div.lean
View file

@ -52,8 +52,6 @@ rfl
notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
lemma modulo.def (a b : ℤ) : a mod b = a - a div b * b := rfl
/- div -/ /- div -/
theorem of_nat_div (m n : nat) : of_nat (m div n) = (of_nat m) div (of_nat n) := theorem of_nat_div (m n : nat) : of_nat (m div n) = (of_nat m) div (of_nat n) :=