Commit 2024-05-13 08:49 b99b683c

View on Github →

chore: adapt to multiple goal linter 6 (#12834) Another halfway split of #12381 on the way to #12352.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/CategoryTheory/Category/RelCat.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

Modified Mathlib/Data/Rat/Cast/Lemmas.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

Modified Mathlib/ModelTheory/Skolem.lean

Modified Mathlib/NumberTheory/Dioph.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Norm.lean

Modified Mathlib/NumberTheory/Padics/Hensel.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean