Skip to content

Commit e7e9abd

Browse files
committed
fix(NumberTheory/MahlerMeasure): add missing public section (#32727)
We add the line ``` @[expose] public section ``` which was missing when the file was created in #31732. Co-authored-by: fbarroero <fbarroero@gmail.com>
1 parent 262b886 commit e7e9abd

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

Mathlib/NumberTheory/MahlerMeasure.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ The main purpose of this file is to prove Northcott's Theorem for the Mahler mea
2121
of degree at most `n` and Mahler measure at most `B`.
2222
-/
2323

24+
@[expose] public section
25+
2426
namespace Polynomial
2527

2628
open Int

0 commit comments

Comments
 (0)