Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
License: APACHE
Name | Size | Last Modified |
---|---|---|
archimedean.lean | 10 KB | 2/19/2020, 2:55:14 AM |
archimedean.olean | 81.3 KB | 2/19/2020, 9:44:21 AM |
associated.lean | 27.2 KB | 2/19/2020, 2:55:14 AM |
big_operators.lean | 39.8 KB | 2/19/2020, 2:55:14 AM |
big_operators.olean | 322.5 KB | 2/19/2020, 9:46:52 AM |
category/ | 4 items | 2/19/2020, 2:55:14 AM |
char_p.lean | 8.6 KB | 2/19/2020, 2:55:14 AM |
char_zero.lean | 3.2 KB | 2/19/2020, 2:55:14 AM |
char_zero.olean | 19.2 KB | 2/19/2020, 9:30:25 AM |
commute.lean | 14.2 KB | 2/19/2020, 2:55:14 AM |
continued_fractions/ | 4 items | 2/19/2020, 2:55:14 AM |
default.lean | 182 bytes | 2/19/2020, 2:55:14 AM |
direct_limit.lean | 25.2 KB | 2/19/2020, 2:55:14 AM |
direct_sum.lean | 6.1 KB | 2/19/2020, 2:55:14 AM |
euclidean_domain.lean | 13.7 KB | 2/19/2020, 2:55:14 AM |
field.lean | 10.1 KB | 2/19/2020, 2:55:15 AM |
field.olean | 57.3 KB | 2/19/2020, 9:20:27 AM |
field_power.lean | 9.1 KB | 2/19/2020, 2:55:15 AM |
field_power.olean | 79.6 KB | 2/19/2020, 9:43:37 AM |
floor.lean | 9.8 KB | 2/19/2020, 2:55:14 AM |
floor.olean | 84.9 KB | 2/19/2020, 9:43:36 AM |
free.lean | 15.5 KB | 2/19/2020, 2:55:14 AM |
gcd_domain.lean | 26.2 KB | 2/19/2020, 2:55:14 AM |
geom_sum.lean | 6.2 KB | 2/19/2020, 2:55:14 AM |
group/ | 22 items | 8/7/2020, 5:35:47 PM |
group_power.lean | 29.1 KB | 2/19/2020, 2:55:15 AM |
group_power.olean | 187.2 KB | 2/19/2020, 9:31:55 AM |
lie_algebra.lean | 16.3 KB | 2/19/2020, 2:55:15 AM |
module.lean | 18.1 KB | 2/19/2020, 2:55:15 AM |
opposites.lean | 5.8 KB | 2/19/2020, 2:55:14 AM |
order.lean | 9.6 KB | 2/19/2020, 2:55:14 AM |
order.olean | 34.5 KB | 2/19/2020, 3:12:43 AM |
order_functions.lean | 13.2 KB | 2/19/2020, 2:55:14 AM |
order_functions.olean | 61.9 KB | 2/19/2020, 9:20:56 AM |
ordered_field.lean | 9.3 KB | 2/19/2020, 2:55:14 AM |
ordered_field.olean | 43.5 KB | 2/19/2020, 9:21:28 AM |
ordered_group.lean | 28.1 KB | 2/19/2020, 2:55:14 AM |
ordered_group.olean | 319.4 KB | 2/19/2020, 9:20:35 AM |
ordered_ring.lean | 21.7 KB | 2/19/2020, 2:55:14 AM |
ordered_ring.olean | 316.7 KB | 2/19/2020, 9:21:14 AM |
pi_instances.lean | 19.2 KB | 2/19/2020, 2:55:14 AM |
pointwise.lean | 12.4 KB | 2/19/2020, 2:55:14 AM |
punit_instances.lean | 3.4 KB | 2/19/2020, 2:55:14 AM |
quadratic_discriminant.lean | 6.4 KB | 2/19/2020, 2:55:14 AM |
ring.lean | 25.6 KB | 2/19/2020, 2:55:15 AM |
ring.olean | 242.4 KB | 2/19/2020, 9:20:20 AM |
semiconj.lean | 8.7 KB | 2/19/2020, 2:55:14 AM |