chore: add 'public section' in Data/Vector/Algebra

2026-03-27 15:24:17 +00:00 · 2025-07-28 22:54:09 +10:00
1 changed files with 6 additions and 2 deletions
--- a/src/Init/Data/Vector/Algebra.lean
+++ b/src/Init/Data/Vector/Algebra.lean
@@ -6,13 +6,15 @@ Authors: Kim Morrison
 module

 prelude
-import Init.Data.Vector.Lemmas
-import Init.Grind
+public import Init.Data.Vector.Lemmas
+public import Init.Grind

 /-!
 # Componentwise algebraic structures on `Vector α n`.
 -/

+public section
+
 namespace Vector

 /-- The zero vector. -/
@@ -168,3 +170,5 @@ instance [NatModule α] [NoNatZeroDivisors α] : NoNatZeroDivisors (Vector α n)
 end grind_instances

 end Vector
+
+end