diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean index be5bbfe8..c4f26e4c 100644 --- a/tests/CompPolyTests.lean +++ b/tests/CompPolyTests.lean @@ -34,6 +34,7 @@ public import CompPolyTests.Fields.Extension.Arithmetic public import CompPolyTests.Fields.Extension.Binomial public import CompPolyTests.Fields.KoalaBear.Fast public import CompPolyTests.Fields.Mersenne31.Fast +public import CompPolyTests.Fields.Mersenne31.Instances public import CompPolyTests.Fields.PrattCertificate public import CompPolyTests.LinearAlgebra.Dense public import CompPolyTests.Multilinear.Equiv diff --git a/tests/CompPolyTests/Fields/Mersenne31/Fast.lean b/tests/CompPolyTests/Fields/Mersenne31/Fast.lean index 954aaa3f..0d305c9d 100644 --- a/tests/CompPolyTests/Fields/Mersenne31/Fast.lean +++ b/tests/CompPolyTests/Fields/Mersenne31/Fast.lean @@ -40,5 +40,7 @@ namespace Mersenne31.Fast #guard toNat ((37 : Field) / 37) = 1 #guard toField ((37 : Field)⁻¹) = ((37 : Mersenne31.Field)⁻¹) #guard toField ((37 : Field) ^ (-3 : Int)) = ((37 : Mersenne31.Field) ^ (-3 : Int)) +#guard ringEquiv ((123 : Field) + 456) = ((123 : Mersenne31.Field) + 456) +#guard ringEquiv ((123 : Field) * 456) = ((123 : Mersenne31.Field) * 456) end Mersenne31.Fast diff --git a/tests/CompPolyTests/Fields/Mersenne31/Instances.lean b/tests/CompPolyTests/Fields/Mersenne31/Instances.lean new file mode 100644 index 00000000..134939fd --- /dev/null +++ b/tests/CompPolyTests/Fields/Mersenne31/Instances.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2026 CompPoly Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Adrien Lacombe +-/ +module + +public import CompPoly.Fields.Mersenne31.Fast + +/-! +# Mersenne31 Field Instance Tests + +Regression checks for the canonical and fast Mersenne31 field instances. +-/ + +public section + +namespace Mersenne31 + +example : Fact (Nat.Prime fieldSize) := inferInstance + +example : _root_.Field Field := inferInstance + +example : NonBinaryField Field := inferInstance + +example : (2 : Field) ≠ 0 := by + exact NonBinaryField.char_neq_2 + +end Mersenne31 + +namespace Mersenne31.Fast + +example : _root_.Field Field := inferInstance + +example : NonBinaryField Field := inferInstance + +end Mersenne31.Fast