From 8072fdf9a0b31abb9d43ab894d7a858639e20ed7 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 1 Oct 2018 16:13:23 -0400 Subject: [PATCH] linkfix closes #11 --- hott/algebra/algebra.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md index d5b2f0bd0..393f3be44 100644 --- a/hott/algebra/algebra.md +++ b/hott/algebra/algebra.md @@ -16,7 +16,7 @@ The following files are [ported](../port.md) from the standard library. If anyth * [ordered_field](ordered_field.hlean) * [bundled](bundled.hlean) : bundled versions of the algebraic structures * [homomorphism](homomorphism.hlean) -* [group_power](group_power.lean) (depends on files in [nat](../types/nat/nat.md) and [int](../types/int/int.md)) +* [group_power](group_power.hlean) (depends on files in [nat](../types/nat/nat.md) and [int](../types/int/int.md)) Files which are not ported from the standard library: