Skip to content

Commit 24d8e80

Browse files
RaggedRclaude
andcommitted
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. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 0c9a79d commit 24d8e80

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)