Commit 2024-08-27 16:57 afa0e97d

View on Github →

chore(Logic/Equiv/Fin): Tidy tuple equivalences (#14665) The names here were all over the place and there were missing versions. Harmonise the names and add the missing versions.

Estimated changes

Modified Archive/Wiedijk100Theorems/CubingACube.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

Modified Mathlib/Data/Countable/Basic.lean

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

added theorem Fin.exists_iff_castSucc

added theorem Fin.exists_iff_succAbove

added theorem Fin.forall_iff_castSucc

modified theorem Fin.forall_iff_succAbove

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

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/Logic/Equiv/Fin.lean

added def Fin.consEquiv

added def Fin.insertNthEquiv

added theorem Fin.insertNthEquiv_last

added theorem Fin.insertNthEquiv_zero

added def Fin.snocEquiv

Modified Mathlib/MeasureTheory/Integral/Pi.lean

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/Order/Fin/Tuple.lean

added def Fin.consOrderIso

added def Fin.insertNthOrderIso

added theorem Fin.insertNthOrderIso_last

added theorem Fin.insertNthOrderIso_zero

added def Fin.snocOrderIso

Modified Mathlib/RepresentationTheory/Action/Monoidal.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean