Commit 2024-05-30 15:41 adeba5c9

View on Github →

style: fix some mis-placed by (#13203)

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Modified Mathlib/Algebra/ContinuedFractions/Translations.lean

modified theorem GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none

Modified Mathlib/Algebra/DirectSum/Ring.lean

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

modified theorem Finset.gcd_image

modified theorem Finset.lcm_image

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/FieldTheory/NormalClosure.lean

modified theorem IntermediateField.normalClosure_of_normal

modified theorem IntermediateField.normal_iff_forall_fieldRange_le

modified theorem IntermediateField.normal_iff_forall_map_le'

modified theorem IntermediateField.normal_iff_forall_map_le

Modified Mathlib/SetTheory/Cardinal/Finite.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Tactic/SimpRw.lean

Modified test/CategoryTheory/Coherence.lean

Modified test/LibrarySearch/basic.lean

Modified test/MoveAdd.lean

Modified test/SimpRw.lean

Modified test/Simps.lean

Modified test/Tauto.lean

Modified test/dfinsupp_notation.lean

Modified test/finsupp_notation.lean

Modified test/matrix.lean

Modified test/norm_cast.lean

Modified test/norm_num.lean