feat(Logic/Equiv/Fin): add finRotate lemma
#22251
Open
+47
−0
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
Paul-Lez
commented
Feb 24, 2025
Paul-Lez
commented
Paul-Lez
added
the
easy
github-actions
bot
added
the
new-contributor
PR summary d8a9743d36
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Logic.Equiv.Fin | 362 | 368 | +6 (+1.66%) |
Import changes for all files
| Files | Import difference |
|---|---|
794 filesMathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Algebra.Spectrum Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.BigOperators.Finsupp Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.Subring Mathlib.Algebra.Colimit.Module Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.Card Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Floor.Prime Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.Sequence Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.Oscillation Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Subadditive Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.CofilteredSystem Mathlib.CategoryTheory.Comma.CardinalArrow Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.Spaces Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.Combinatorics.Derangements.Basic Mathlib.Combinatorics.Derangements.Finite Mathlib.Combinatorics.Enumerative.Bell Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Combinatorics.Enumerative.Composition Mathlib.Combinatorics.Enumerative.DyckWord Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.Hall.Basic Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Computability.Encoding Mathlib.Computability.TMComputable Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Data.Fin.Tuple.Reflection Mathlib.Data.FinEnum.Option Mathlib.Data.Finset.Finsupp Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.Encodable Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.SMul Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Data.Finsupp.Weight Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Int.CardIntervalMod Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.ConjTranspose Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Notation Mathlib.Data.Matrix.Reflection Mathlib.Data.Matrix.RowCol Mathlib.Data.Nat.Choose.Cast Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Count Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Nth Mathlib.Data.Nat.Prime.Nth Mathlib.Data.Nat.Squarefree Mathlib.Data.Rat.Cardinal Mathlib.Data.W.Cardinal Mathlib.Deprecated.Cardinal.Continuum Mathlib.Deprecated.Cardinal.PartENat Mathlib.Dynamics.Flow Mathlib.Dynamics.Minimal Mathlib.Dynamics.OmegaLimit Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.CoprodI Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.MonoidLocalization.Cardinality Mathlib.GroupTheory.OreLocalization.Cardinality Mathlib.GroupTheory.Perm.Option Mathlib.GroupTheory.Perm.Sign Mathlib.InformationTheory.Hamming Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Hydra Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Basic Mathlib.ModelTheory.Bundled Mathlib.ModelTheory.Complexity Mathlib.ModelTheory.Definability Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Encoding Mathlib.ModelTheory.Equivalence Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.Fraisse Mathlib.ModelTheory.Graph Mathlib.ModelTheory.LanguageMap Mathlib.ModelTheory.Order Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Satisfiability Mathlib.ModelTheory.Semantics Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Syntax Mathlib.ModelTheory.Types Mathlib.ModelTheory.Ultraproducts Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.Primorial Mathlib.NumberTheory.SmoothNumbers Mathlib.Order.Extension.Well Mathlib.Order.Filter.CardinalInter Mathlib.Order.Filter.Cocardinal Mathlib.Order.Filter.ENNReal Mathlib.Order.JordanHolder Mathlib.Order.Monotone.MonovaryOrder Mathlib.Order.Partition.Equipartition Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.Radical Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.SetTheory.Cardinal.Aleph Mathlib.SetTheory.Cardinal.Arithmetic Mathlib.SetTheory.Cardinal.Basic Mathlib.SetTheory.Cardinal.Cofinality Mathlib.SetTheory.Cardinal.Continuum Mathlib.SetTheory.Cardinal.CountableCover Mathlib.SetTheory.Cardinal.Divisibility Mathlib.SetTheory.Cardinal.ENat Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Cardinal.HasCardinalLT Mathlib.SetTheory.Cardinal.Subfield Mathlib.SetTheory.Cardinal.ToNat Mathlib.SetTheory.Cardinal.UnivLE Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Nimber.Basic Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.SetTheory.Ordinal.Basic Mathlib.SetTheory.Ordinal.CantorNormalForm Mathlib.SetTheory.Ordinal.Enum Mathlib.SetTheory.Ordinal.Exponential Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.SetTheory.Ordinal.Notation Mathlib.SetTheory.Ordinal.Principal Mathlib.SetTheory.Ordinal.Rank Mathlib.SetTheory.Ordinal.Topology Mathlib.SetTheory.Ordinal.Veblen Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.Surreal.Dyadic Mathlib.SetTheory.Surreal.Multiplication Mathlib.SetTheory.ZFC.Rank Mathlib.Tactic.ComputeDegree Mathlib.Testing.Plausible.Functions Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Topology.Algebra.Constructions Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.IntermediateField Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.Floor Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Star Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Topology.Algebra.UniformGroup.Defs Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.ULift Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Category.UniformSpace Mathlib.Topology.ClopenBox Mathlib.Topology.CompactOpen Mathlib.Topology.Compactification.OnePoint Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Constructible Mathlib.Topology.ContinuousMap.Basic Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.ContinuousMap.Sigma Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.Covering Mathlib.Topology.DiscreteQuotient Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.FiberPartition Mathlib.Topology.Gluing Mathlib.Topology.Hom.Open Mathlib.Topology.Homeomorph Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.ENNReal.Defs Mathlib.Topology.Instances.ENat Mathlib.Topology.Instances.EReal.Defs Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.NNReal.Defs Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.Real.Defs Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.JacobsonSpace Mathlib.Topology.KrullDimension Mathlib.Topology.List Mathlib.Topology.LocalAtTarget Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Maps.Proper.Basic Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.NoetherianSpace Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.Order.ScottTopology Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Topology.PartialHomeomorph Mathlib.Topology.Path Mathlib.Topology.QuasiSeparated Mathlib.Topology.Sequences Mathlib.Topology.Sets.Closeds Mathlib.Topology.Sets.Compacts Mathlib.Topology.Sets.Opens Mathlib.Topology.Sets.Order Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Sheaves.Presheaf Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.Sober Mathlib.Topology.Specialization Mathlib.Topology.Spectral.Hom Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Cauchy Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.UnitInterval |
1 |
4 filesMathlib.Data.Fin.Tuple.Curry Mathlib.Logic.Equiv.Fin Mathlib.Order.Fin.Finset Mathlib.Order.Fin.Tuple |
6 |
Declarations diff
+ coe_finRotate_symm_of_ne_zero
+ finRotate_succ_symm_apply
+ finRotate_symm_lt_iff_ne_zero
+ lt_finRotate_iff_ne_last
+ one_le_of_ne_zero
+ val_eq_zero_iff
+ val_ne_zero_iff
+ val_sub_one_of_ne_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
eric-wieser
reviewed
Feb 24, 2025
added 3 commits
February 25, 2025 10:26
eric-wieser
reviewed
Feb 25, 2025
Mathlib/Data/Fin/Basic.lean
Outdated
Comment on lines
150
to
152
| lemma val_ne_zero_iff {n : ℕ} {k : Fin (n+1)} : | ||
| k ≠ 0 ↔ (k : ℕ) ≠ 0 := by | ||
| rw [←Fin.val_ne_iff, Fin.val_zero] |
There was a problem hiding this comment.
This lemma is backwards, val_ne refers to the RHS not the LHS.
Can you also add the val_eq_zero_iff version, and mark both norm_cast and the = one simp?
eric-wieser
reviewed
Feb 25, 2025
| · simp only [hc, finRotate_succ_apply, Fin.last_add_one, Fin.not_lt_zero] at hi | ||
| · rw [Fin.lt_iff_val_lt_val, coe_finRotate_of_ne_last hi, Nat.lt_add_one_iff] | ||
|
|
||
| lemma finRotate_succ_symm_apply (i : Fin n.succ) : |
There was a problem hiding this comment.
I think this should be stated with NeZero n and Fin n
There was a problem hiding this comment.
In that case should I also restate finRotate_succ_apply ?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.