Commit 2024-11-18 11:19 db944bfd

View on Github →

chore: use Pairwise (_ on _) where possible (#9256)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

Modified Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Modified Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Permutation.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Multiset/Bind.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/Data/Set/Lattice.lean

modified theorem Set.sigmaToiUnion_bijective

modified theorem Set.sigmaToiUnion_injective

Modified Mathlib/Data/Setoid/Partition.lean

modified theorem IndexedPartition.disjoint

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean