Skip to content

Commit c66ed86

Browse files
committed
fix: add module declaration for Lean 4.30.0 compatibility
Adds `module` keyword and changes `import` to `public import` to match the module system introduced in Lean 4.30.0-rc2, which Mathlib master now requires.
1 parent ccfd155 commit c66ed86

1 file changed

Lines changed: 6 additions & 4 deletions

File tree

Mathlib/RingTheory/HopfAlgebra/Polynomial.lean

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,12 @@ Copyright (c) 2025 Robin Langer. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robin Langer
55
-/
6-
import Mathlib.RingTheory.HopfAlgebra.Basic
7-
import Mathlib.Algebra.Polynomial.AlgebraMap
8-
import Mathlib.Algebra.Polynomial.Eval.SMul
9-
import Mathlib.RingTheory.TensorProduct.Maps
6+
module
7+
8+
public import Mathlib.RingTheory.HopfAlgebra.Basic
9+
public import Mathlib.Algebra.Polynomial.AlgebraMap
10+
public import Mathlib.Algebra.Polynomial.Eval.SMul
11+
public import Mathlib.RingTheory.TensorProduct.Maps
1012

1113
/-!
1214
# The Hopf algebra structure on polynomials (additive group scheme 𝔾ₐ)

0 commit comments

Comments
 (0)