Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-20 10:08
db5a9376
View on Github →
chore: Remove unnecessary "rw"s (
#10704
) Remove unnecessary "rw"s.
Estimated changes
Modified
Mathlib/Algebra/Algebra/Operations.lean
Modified
Mathlib/Algebra/BigOperators/Basic.lean
Modified
Mathlib/Algebra/DirectSum/Algebra.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.lean
Modified
Mathlib/Algebra/Quandle.lean
modified
theorem
UnitalShelf.act_idem
Modified
Mathlib/Algebra/Regular/Basic.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Split.lean
Modified
Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
Modified
Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
Modified
Mathlib/CategoryTheory/Localization/Composition.lean
Modified
Mathlib/Data/Int/Cast/Basic.lean
Modified
Mathlib/Data/List/Rotate.lean
Modified
Mathlib/Data/Num/Lemmas.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/Polynomial/Eval.lean
Modified
Mathlib/Data/Polynomial/Monic.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Init/Data/Nat/Bitwise.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
Modified
Mathlib/LinearAlgebra/Basis.lean
Modified
Mathlib/LinearAlgebra/Dimension/Constructions.lean
Modified
Mathlib/Logic/Equiv/List.lean
Modified
Mathlib/Logic/Function/Basic.lean
Modified
Mathlib/MeasureTheory/Group/AddCircle.lean
Modified
Mathlib/MeasureTheory/Measure/OuterMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/VectorMeasure.lean
Modified
Mathlib/NumberTheory/BernoulliPolynomials.lean
Modified
Mathlib/NumberTheory/DiophantineApproximation.lean
Modified
Mathlib/NumberTheory/NumberField/Embeddings.lean
Modified
Mathlib/NumberTheory/RamificationInertia.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/SymmDiff.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
Modified
Mathlib/RingTheory/IsTensorProduct.lean
Modified
Mathlib/RingTheory/Norm.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
Modified
Mathlib/RingTheory/Polynomial/Pochhammer.lean
Modified
Mathlib/RingTheory/Trace.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean