9 lines
132 B
Text
9 lines
132 B
Text
|
import data.int data.real
|
|||
|
|
open int real
|
|||
|
|
|
|||
|
|
example : (1 : ℤ) * (1 : ℤ) = (1 : ℤ) :=
|
|||
|
|
sorry
|
|||
|
|
|
|||
|
|
example : (1 : ℤ) * 1 = 1 :=
|
|||
|
|
sorry
|