Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-08 13:31
0fe74732
View on Github →
chore(Algebra/CharP/Basic): don't import
IsSimpleRing
(
#20550
)
Estimated changes
Modified
Mathlib/Algebra/Algebra/ZMod.lean
Modified
Mathlib/Algebra/CharP/Algebra.lean
deleted
theorem
Algebra.charP_iff
deleted
theorem
RingHom.charP_iff
added
theorem
RingHom.charP_iff_charP
Modified
Mathlib/Algebra/CharP/Basic.lean
deleted
theorem
RingHom.charP_iff_charP
Modified
Mathlib/Algebra/Homology/Bifunctor.lean
Modified
Mathlib/Algebra/Homology/BifunctorAssociator.lean
Modified
Mathlib/Algebra/Homology/BifunctorHomotopy.lean
Modified
Mathlib/Algebra/Homology/BifunctorShift.lean
Modified
Mathlib/Algebra/Homology/ComplexShapeSigns.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
Modified
Mathlib/Algebra/Homology/Monoidal.lean
Modified
Mathlib/Algebra/Homology/TotalComplex.lean
Modified
Mathlib/Algebra/Homology/TotalComplexShift.lean
Modified
Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
Modified
Mathlib/Algebra/Module/ZMod.lean
Modified
Mathlib/Algebra/Order/ToIntervalMod.lean
Modified
Mathlib/Algebra/Periodic.lean
Modified
Mathlib/Algebra/Ring/NegOnePow.lean
Modified
Mathlib/CategoryTheory/Localization/Triangulated.lean
Modified
Mathlib/CategoryTheory/Sites/SheafCohomology/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Adjunction.lean
Modified
Mathlib/CategoryTheory/Triangulated/Functor.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Subcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
Modified
Mathlib/CategoryTheory/Triangulated/Triangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Yoneda.lean
Modified
Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
Modified
Mathlib/Combinatorics/Additive/Corner/Defs.lean
Modified
Mathlib/Combinatorics/Additive/FreimanHom.lean
Modified
Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Matching.lean
Modified
Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean
Modified
Mathlib/Data/Nat/Periodic.lean
Modified
Mathlib/Data/ZMod/Aut.lean
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/Data/ZMod/Coprime.lean
Modified
Mathlib/Data/ZMod/Factorial.lean
Modified
Mathlib/Data/ZMod/IntUnitsPower.lean
Modified
Mathlib/Data/ZMod/Units.lean
Modified
Mathlib/FieldTheory/Perfect.lean
Modified
Mathlib/GroupTheory/CommutingProbability.lean
Modified
Mathlib/GroupTheory/Coxeter/Inversion.lean
Modified
Mathlib/GroupTheory/Coxeter/Length.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
Modified
Mathlib/NumberTheory/FLT/Four.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/PythagoreanTriples.lean
Modified
Mathlib/RingTheory/Polynomial/Dickson.lean