Lean’s core library has no support for rational or real numbers 😦

They are however in the maths library — or we can just make some fake real numbers and use them instead.

-- let's define the real numbers to be a number system which satisfies

-- the basic properties of the real numbers which we will need.

```
```noncomputable theory

constant real : Type

@[instance] constant real_field : linear_ordered_field real

-- This piece of magic means that "real" now behaves a lot like

-- the real numbers. In particular we now have a bunch

-- of theorems:

example : ∀ x y : real, x * y = y * x := mul_comm

`#check mul_assoc`

At Imperial I’ve just been talking to the 1st years about taking a rational power of a positive real number. I guess we could set all this up in Lean.

open nat

```
```definition natural_power : real → nat → real

| x 0 := 1

| x (n+1) := (natural_power x n) * x

`theorem power_comm : ∀ x:real, ∀ m n:nat, natural_power x (m+n) = natural_power x m *natural_power x n :=`

begin

admit

end

That’s a definition (by recursion) of for real and a non-negative integer. It’s also a theorem which needs proving. We can prove that theorem by induction, I suspect. I’ll try it later on.

But what I really want is a rational power. We’re going to need existence of positive th roots.

constant nth_root (x : real) (n : nat) : (x>0) → (n>0) → real

```
```

`axiom is_nth_root (x : real) (n : nat) (Hx : x>0) (Hn : n>0) : natural_power (nth_root x n Hx Hn) n = x`

Now we can consider trying to define rational powers!

constant nth_root (x : real) (n : nat) : (x>0) → (n>0) → real

```
```axiom is_nth_root (x : real) (n : nat) (Hx : x>0) (Hn : n>0) : natural_power (nth_root x n Hx Hn) n = x

`definition rational_power_v0 (x : real) (n : nat) (d : nat) (Hx : x > 0) (Hd : d > 0) : real :=`

natural_power (nth_root x d Hx Hd) n

This code is now up on xena’s github:

link to rational power stuff

Let’s see what we can do with it!

### Like this:

Like Loading...

*Related*

## About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.