Commit 2025-02-14 05:38 3b08f315

View on Github →

chore(Data/ZMod/Basic): don't import Field (#21317)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Field/NegOnePow.lean

added theorem Int.cast_negOnePow

Created Mathlib/Algebra/Field/ZMod.lean

Modified Mathlib/Algebra/Homology/ComplexShapeSigns.lean

Modified Mathlib/Algebra/Ring/NegOnePow.lean

deleted theorem Int.cast_negOnePow

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

Modified Mathlib/Data/ZMod/Aut.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/NumberTheory/LucasPrimality.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/Polynomial/Dickson.lean

Modified MathlibTest/instance_diamonds.lean