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