Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(Algebra/Group/Defs): use Nat.binaryRec #17892

Open
wants to merge 49 commits into
base: master
Choose a base branch
from

Conversation

FR-vdash-bot
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot commented Oct 18, 2024

@FR-vdash-bot FR-vdash-bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 18, 2024
Copy link

github-actions bot commented Oct 18, 2024

PR summary 7104392807

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.Group.Defs 70 71 +1 (+1.43%)
Import changes for all files
Files Import difference
1374 files Mathlib.Algebra.Homology.ShortComplex.LeftHomology Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.WithOne.Defs Mathlib.Tactic.Ring.Basic Mathlib.Order.Partition.Equipartition Mathlib.Data.Nat.Hyperoperation Mathlib.Algebra.Group.Units.Defs Mathlib.CategoryTheory.Category.PartialFun Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.CategoryTheory.Abelian.Generator Mathlib.Algebra.Order.Monoid.Defs Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.Data.Int.Associated Mathlib.CategoryTheory.Limits.Constructions.Filtered Mathlib.Combinatorics.Additive.ETransform Mathlib.LinearAlgebra.BilinearMap Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Order.Filter.Germ.Basic Mathlib.Algebra.Order.Monoid.Units Mathlib.Data.Multiset.Sum Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Control.Traversable.Instances Mathlib.Algebra.Ring.Action.Invariant Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Control.Fix Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.Data.Multiset.Nodup Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.Data.LazyList.Basic Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.Algebra.Group.Commute.Hom Mathlib.GroupTheory.Commutator.Basic Mathlib.GroupTheory.Congruence.Hom Mathlib.Tactic.FunProp Mathlib.Data.Finset.PiInduction Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.Algebra.Group.Hom.Basic Mathlib.Data.NNRat.Order Mathlib.Algebra.Homology.ShortComplex.RightHomology Mathlib.Algebra.BigOperators.Finsupp Mathlib.Algebra.BigOperators.RingEquiv Mathlib.Data.Finset.Interval Mathlib.Algebra.PUnitInstances.Order Mathlib.Data.Fintype.Fin Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels Mathlib.CategoryTheory.Limits.Shapes.KernelPair Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Data.Fintype.Sum Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Algebra.GCDMonoid.Nat Mathlib.Order.Disjointed Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.CategoryTheory.FintypeCat Mathlib.Algebra.GradedMonoid Mathlib.Data.Fintype.Powerset Mathlib.Algebra.IsPrimePow Mathlib.CategoryTheory.Shift.Predicate Mathlib.CategoryTheory.Closed.FunctorCategory Mathlib.GroupTheory.SemidirectProduct Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.Data.Multiset.Sym Mathlib.Order.Grade Mathlib.Combinatorics.Enumerative.DyckWord Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Data.Int.Cast.Field Mathlib.Algebra.Order.Sub.Defs Mathlib.Data.NNRat.BigOperators Mathlib.CategoryTheory.Monoidal.Skeleton Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Group.Units Mathlib.Tactic.NormNum.Prime Mathlib.Data.Nat.Cast.WithTop Mathlib.Order.FixedPoints Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Algebra.Divisibility.Units Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Ring.Subring.Order Mathlib.Algebra.Star.Pointwise Mathlib.Data.PNat.Find Mathlib.Data.Nat.WithBot Mathlib.Data.Finset.Grade Mathlib.Algebra.Order.Ring.Basic Mathlib.Tactic.Positivity.Finset Mathlib.Algebra.Group.Action.Option Mathlib.Combinatorics.Additive.DoublingConst Mathlib.Combinatorics.SimpleGraph.LineGraph Mathlib.GroupTheory.Submonoid.Center Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.Algebra.Homology.Functor Mathlib.Data.Nat.Cast.Prod Mathlib.Algebra.Module.Submodule.Basic Mathlib.NumberTheory.Primorial Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Tactic.IntervalCases Mathlib.Algebra.Group.Fin.Tuple Mathlib.Data.Finsupp.Basic Mathlib.Algebra.Order.Algebra Mathlib.Data.DFinsupp.Multiset Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts Mathlib.Algebra.Order.Star.Basic Mathlib.GroupTheory.Congruence.Opposite Mathlib.Algebra.Category.Ring.Colimits Mathlib.Data.SetLike.Fintype Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.CategoryTheory.Limits.Shapes.Kernels Mathlib.Algebra.Group.Commutator Mathlib.CategoryTheory.Limits.TypesFiltered Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Algebra.CharZero.Lemmas Mathlib.Data.Rat.Defs Mathlib.Data.FinEnum Mathlib.Data.Int.Cast.Prod Mathlib.Data.Multiset.Antidiagonal Mathlib.Algebra.Homology.Additive Mathlib.Data.Vector3 Mathlib.Tactic.Ring.PNat Mathlib.Data.List.EditDistance.Defs Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Algebra.Module.Algebra Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.RingTheory.TwoSidedIdeal.BigOperators Mathlib.Data.Fin.Tuple.Finset Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Star.StarRingHom Mathlib.GroupTheory.Subsemigroup.Center Mathlib.Data.Finset.Option Mathlib.Data.Fintype.Quotient Mathlib.CategoryTheory.Localization.FiniteProducts Mathlib.Tactic.Linarith.Preprocessing Mathlib.RingTheory.Prime Mathlib.Algebra.Order.Monoid.ToMulBot Mathlib.CategoryTheory.Subobject.Limits Mathlib.Data.DFinsupp.Basic Mathlib.Algebra.Group.Commute.Defs Mathlib.Order.Filter.Basic Mathlib.Order.RelIso.Group Mathlib.CategoryTheory.Monoidal.Linear Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.Logic.Small.List Mathlib.Data.Set.Pointwise.Iterate Mathlib.Data.String.Basic Mathlib.Algebra.Order.Group.MinMax Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.Order.CompleteSublattice Mathlib.GroupTheory.Perm.Sign Mathlib.Tactic.LinearCombination Mathlib.RingTheory.Multiplicity Mathlib.Data.ENat.Basic Mathlib.Algebra.Group.Action.Pi Mathlib.CategoryTheory.Endomorphism Mathlib.Data.Int.AbsoluteValue Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Data.Multiset.Functor Mathlib.Algebra.Ring.Fin Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Order.Pi Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Tactic.Positivity.Core Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.Order.Interval.Finset.Fin Mathlib.GroupTheory.Perm.ViaEmbedding Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Monad.Monadicity Mathlib.Data.Int.Order.Lemmas Mathlib.Algebra.Group.Prod Mathlib.Data.Finsupp.Notation Mathlib.CategoryTheory.SingleObj Mathlib.Combinatorics.Enumerative.Composition Mathlib.Algebra.Order.Field.Pointwise Mathlib.CategoryTheory.ConcreteCategory.EpiMono Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Control.Applicative Mathlib.Algebra.Group.Invertible.Basic Mathlib.GroupTheory.Subgroup.Center Mathlib.Algebra.Order.Field.InjSurj Mathlib.Algebra.Category.Semigrp.Basic Mathlib.GroupTheory.Perm.List Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.Equiv.Basic Mathlib.Data.Fintype.Option Mathlib.Algebra.Homology.ShortComplex.PreservesHomology Mathlib.NumberTheory.Divisors Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Tactic.Positivity Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.Tactic.FunProp.RefinedDiscrTree Mathlib.CategoryTheory.GlueData Mathlib.Data.Finset.Lattice Mathlib.CategoryTheory.GradedObject.Monoidal Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Limits.Preserves.Opposites Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows Mathlib.Algebra.Order.Group.Synonym Mathlib.CategoryTheory.Dialectica.Basic Mathlib.Algebra.Order.GroupWithZero.Action.Synonym Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Filtered.Final Mathlib.Algebra.Group.Nat Mathlib.Dynamics.PeriodicPts Mathlib.Algebra.Homology.ShortComplex.Basic Mathlib.CategoryTheory.Sites.Preserves Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Interval.Set.Group Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.Tactic.RewriteSearch Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Quasicategory Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.RingTheory.Congruence.BigOperators Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Tactic.FunProp.Elab Mathlib.NumberTheory.ADEInequality Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Group.ULift Mathlib.CategoryTheory.Limits.Shapes.FunctorCategory Mathlib.Tactic.NormNum.Basic Mathlib.Algebra.Order.Group.Indicator Mathlib.GroupTheory.Perm.Support Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.AlgebraicTopology.CechNerve Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Abelian.Opposite Mathlib.Order.JordanHolder Mathlib.CategoryTheory.Preadditive.Generator Mathlib.Data.Nat.Cast.Field Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.CategoryTheory.Abelian.GrothendieckAxioms Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Data.Finsupp.Fin Mathlib.Order.Part Mathlib.Data.Set.Pointwise.Interval Mathlib.Data.Real.Sign Mathlib.Data.Int.NatPrime Mathlib.Deprecated.Submonoid Mathlib.Data.Nat.Cast.Order.Field Mathlib.Algebra.Ring.Aut Mathlib.Algebra.GroupWithZero.Basic Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.Data.Nat.GCD.BigOperators Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.CategoryTheory.Closed.Ideal Mathlib.Algebra.Order.Nonneg.Ring Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Order.Sub.WithTop Mathlib.Data.PFun Mathlib.Algebra.Star.Pi Mathlib.Algebra.Homology.HomologicalComplex Mathlib.GroupTheory.EckmannHilton Mathlib.Order.Interval.Multiset Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Group.EvenFunction Mathlib.CategoryTheory.Preadditive.Projective Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.BigOperators.Group.Finset Mathlib.CategoryTheory.Sites.Continuous Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Group.Instances Mathlib.CategoryTheory.Localization.Pi Mathlib.Algebra.Group.NatPowAssoc Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Fintype.Parity Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Data.Finset.Image Mathlib.Algebra.Ring.WithZero Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.Module.Submodule.Range Mathlib.CategoryTheory.Monad.Equalizer Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Algebra.Field.MinimalAxioms Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Algebra.BigOperators.Pi Mathlib.Algebra.Order.Ring.Finset Mathlib.CategoryTheory.Monoidal.Center Mathlib.Algebra.Quandle Mathlib.Algebra.Module.Basic Mathlib.Data.Fintype.Order Mathlib.Order.Birkhoff Mathlib.CategoryTheory.Filtered.Basic Mathlib.Algebra.Ring.Equiv Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.CategoryTheory.Triangulated.Basic Mathlib.NumberTheory.Harmonic.Defs Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.Data.Nat.Pairing Mathlib.Data.Finset.Fin Mathlib.Algebra.Order.GroupWithZero.WithZero Mathlib.Algebra.Ring.Subring.Basic Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Data.Finset.Sum Mathlib.Algebra.Order.SuccPred.TypeTags Mathlib.Algebra.GroupWithZero.Center Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Ring.Centralizer Mathlib.CategoryTheory.Limits.Constructions.Over.Products Mathlib.Data.Set.MemPartition Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.Algebra.Order.Module.Synonym Mathlib.Tactic.NormNum.Core Mathlib.CategoryTheory.Limits.Presheaf Mathlib.Algebra.Group.Int Mathlib.RingTheory.TwoSidedIdeal.Lattice Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.Data.Rat.Lemmas Mathlib.Data.Nat.Cast.Defs Mathlib.Order.Interval.Set.Infinite Mathlib.Data.Nat.Upto Mathlib.Order.OmegaCompletePartialOrder Mathlib.Tactic.Sat.FromLRAT Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Data.Finsupp.Defs Mathlib.Data.Finset.Pi Mathlib.Data.DFinsupp.NeLocus Mathlib.Data.Finset.Powerset Mathlib.Algebra.Ring.Commute Mathlib.Order.Category.OmegaCompletePartialOrder Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.Algebra.Group.Pointwise.Finset.Basic Mathlib.LinearAlgebra.GeneralLinearGroup Mathlib.Combinatorics.Additive.Energy Mathlib.Algebra.Order.Interval.Multiset Mathlib.CategoryTheory.Closed.Functor Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.CategoryTheory.Shift.Quotient Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.Order.Filter.Germ.OrderedMonoid Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.GroupWithZero.Invertible Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts Mathlib.Data.Set.Equitable Mathlib.Algebra.GCDMonoid.Multiset Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.CategoryTheory.Monoidal.Hopf_ Mathlib.Algebra.Ring.Opposite Mathlib.Computability.ContextFreeGrammar Mathlib.Algebra.BigOperators.Ring.List Mathlib.Algebra.Module.LinearMap.Prod Mathlib.GroupTheory.Coprod.Basic Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.Algebra.Star.Prod Mathlib.Data.Int.Interval Mathlib.RingTheory.Coprime.Lemmas Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Ring.Semiconj Mathlib.CategoryTheory.GradedObject.Associator Mathlib.Algebra.Ring.Regular Mathlib.Data.Int.Cast.Defs Mathlib.Data.Finset.Sups Mathlib.Data.Finset.Sym Mathlib.Data.Finset.Piecewise Mathlib.Algebra.Ring.AddAut Mathlib.Algebra.Ring.Pointwise.Finset Mathlib.SetTheory.Game.Basic Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Algebra.EuclideanDomain.Int Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.FreeMonoid.Basic Mathlib.Data.Set.Pointwise.Support Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.Order.Restriction Mathlib.CategoryTheory.Groupoid.VertexGroup Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.RingTheory.SimpleRing.Defs Mathlib.Algebra.Algebra.Basic Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.Data.Finset.Functor Mathlib.Data.Nat.Factorization.Defs Mathlib.CategoryTheory.Monad.EquivMon Mathlib.Data.Set.Constructions Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Abelian Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.RingTheory.SimpleRing.Basic Mathlib.Dynamics.FixedPoints.Basic Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Order.CompleteLattice.Finset Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Combinatorics.Derangements.Basic Mathlib.Algebra.Category.MonCat.Limits Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero Mathlib.Order.Category.FinBoolAlg Mathlib.Tactic.Polyrith Mathlib.Algebra.Group.Conj Mathlib.Data.Finset.NatAntidiagonal Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Order.Field.Basic Mathlib.CategoryTheory.Abelian.Basic Mathlib.Algebra.Lie.Basic Mathlib.RingTheory.OreLocalization.Basic Mathlib.Algebra.Group.Units.Basic Mathlib.Data.Finset.Update Mathlib.Tactic.Linarith.Frontend Mathlib.Algebra.Group.Defs Mathlib.CategoryTheory.Limits.Constructions.EpiMono Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.BigOperators.Option Mathlib.Tactic.FinCases Mathlib.Algebra.Order.Monovary Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero Mathlib.CategoryTheory.Preadditive.OfBiproducts Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.CategoryTheory.Sites.Localization Mathlib.Tactic.NormNum.BigOperators Mathlib.Algebra.Ring.Subring.Units Mathlib.Data.Rat.BigOperators Mathlib.Data.Nat.ModEq Mathlib.Algebra.Module.Opposites Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks Mathlib.Control.LawfulFix Mathlib.NumberTheory.FrobeniusNumber Mathlib.Data.Pi.Interval Mathlib.Combinatorics.Additive.Dissociation Mathlib.Tactic.LinearCombination.Lemmas Mathlib.Algebra.Field.Opposite Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.Algebra.Field.Defs Mathlib.CategoryTheory.Monoidal.Bimon_ Mathlib.CategoryTheory.Countable Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Center Mathlib.Algebra.GroupWithZero.Action.Basic Mathlib.CategoryTheory.Filtered.Small Mathlib.Algebra.Group.AddChar Mathlib.Data.Finset.Pairwise Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.Algebra.Algebra.Hom.Rat Mathlib.GroupTheory.Perm.Option Mathlib.Algebra.Order.BigOperators.Expect Mathlib.Data.Finsupp.Antidiagonal Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Homology.ShortComplex.Homology Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Ring.WithTop Mathlib.Combinatorics.Additive.PluenneckeRuzsa Mathlib.CategoryTheory.Monad.Comonadicity Mathlib.Tactic.FunProp.Theorems Mathlib.Algebra.BigOperators.Ring.Nat Mathlib.Data.Holor Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.BigOperators.Ring.Multiset Mathlib.Data.Fintype.Sort Mathlib.Algebra.BigOperators.Balance Mathlib.Algebra.Order.Nonneg.Field Mathlib.Algebra.Field.Equiv Mathlib.CategoryTheory.ChosenFiniteProducts.Cat Mathlib.Algebra.Ring.Rat Mathlib.Data.Nat.Dist Mathlib.Data.Ordmap.Ordset Mathlib.Data.Bool.Count Mathlib.GroupTheory.Subgroup.Saturated Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.GroupWithZero.WithZero Mathlib.Algebra.Order.Module.Rat Mathlib.Combinatorics.HalesJewett Mathlib.CategoryTheory.Monoidal.FunctorCategory Mathlib.Data.Fintype.Card Mathlib.Order.Monotone.Odd Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.Data.Setoid.Partition Mathlib.Algebra.Order.Ring.Unbundled.Nonneg Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Order.Interval.Finset.Basic Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset Mathlib.Data.Rat.Cast.Order Mathlib.Algebra.Order.BigOperators.Group.List Mathlib.Data.Multiset.Bind Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Algebra.Opposite Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.Data.Nat.SuccPred Mathlib.Algebra.ContinuedFractions.Translations Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.Data.Matrix.DMatrix Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.Algebra.Group.Equiv.Basic Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.RingTheory.Localization.Integer Mathlib.Algebra.Tropical.Lattice Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Data.Vector.Zip Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.Algebra.Order.Module.Defs Mathlib.Algebra.Order.Nonneg.Module Mathlib.Algebra.Order.CauSeq.Completion Mathlib.Data.Fintype.Basic Mathlib.Algebra.Order.Ring.Star Mathlib.Data.Finset.Slice Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Tactic.Monotonicity Mathlib.CategoryTheory.Limits.Shapes.Diagonal Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.Tropical.Basic Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.Deprecated.Subgroup Mathlib.Data.Finset.Finsupp Mathlib.RingTheory.Localization.Defs Mathlib.Algebra.Module.LinearMap.Basic Mathlib.Algebra.Field.Rat Mathlib.Algebra.Homology.ImageToKernel Mathlib.Data.Rat.Cast.Defs Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.Divisibility.Prod Mathlib.Algebra.Free Mathlib.Data.Array.Lemmas Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Control.Random Mathlib.Order.Filter.Partial Mathlib.CategoryTheory.DifferentialObject Mathlib.CategoryTheory.Abelian.Refinements Mathlib.Data.BitVec Mathlib.CategoryTheory.Monoidal.Mod_ Mathlib.CategoryTheory.Quotient.Linear Mathlib.Algebra.AddTorsor Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Algebra.Ring.Action.Basic Mathlib.LinearAlgebra.AffineSpace.Basic Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.Data.Finset.Max Mathlib.Tactic.Linarith Mathlib.Algebra.Algebra.Pi Mathlib.Data.Nat.Choose.Dvd Mathlib.Control.ULiftable Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.RingTheory.Nilpotent.Defs Mathlib.Order.SupIndep Mathlib.Data.DFinsupp.Interval Mathlib.CategoryTheory.Noetherian Mathlib.Algebra.Module.LinearMap.Defs Mathlib.CategoryTheory.GuitartExact.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Deprecated.Ring Mathlib.Computability.TuringMachine Mathlib.Control.Monad.Writer Mathlib.Order.Irreducible Mathlib.Algebra.Ring.Identities Mathlib.Algebra.BigOperators.Intervals Mathlib.Tactic.CancelDenoms Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.Algebra.Category.GrpWithZero Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.Algebra.Order.GroupWithZero.Canonical Mathlib.Order.Interval.Set.Pi Mathlib.CategoryTheory.Monoidal.Tor Mathlib.Data.List.EditDistance.Estimator Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.Data.Finite.Basic Mathlib.Data.Multiset.FinsetOps Mathlib.Algebra.Group.Aut Mathlib.Algebra.CharP.Defs Mathlib.Data.Sym.Basic Mathlib.RingTheory.TwoSidedIdeal.Basic Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Order.ConditionallyCompleteLattice.Finset Mathlib.Algebra.CharP.Subring Mathlib.Algebra.ContinuedFractions.Basic Mathlib.Algebra.Order.EuclideanAbsoluteValue Mathlib.Combinatorics.Hall.Finite Mathlib.Algebra.GCDMonoid.Basic Mathlib.Testing.SlimCheck.Functions Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Ring.Hom.Basic Mathlib.Data.Set.Semiring Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Invertible Mathlib.Tactic.NormNum.Ineq Mathlib.CategoryTheory.Sites.Limits Mathlib.Data.Vector.Mem Mathlib.Order.Filter.Ker Mathlib.Algebra.Order.Group.Nat Mathlib.Data.Fintype.BigOperators Mathlib.CategoryTheory.ComposableArrows Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Data.Nat.Cast.SetInterval Mathlib.Data.PNat.Prime Mathlib.Data.Set.Enumerate Mathlib.Data.Set.Pointwise.ListOfFn Mathlib.Algebra.Order.Group.Lattice Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.LinearAlgebra.Pi Mathlib.Data.Finsupp.Multiset Mathlib.Data.Vector.MapLemmas Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Algebra.Group.Invertible.Defs Mathlib.RingTheory.TwoSidedIdeal.Instances Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Ring.Action.Group Mathlib.Tactic.Ring.RingNF Mathlib.Algebra.Order.Star.Conjneg Mathlib.Algebra.Order.Field.Canonical.Defs Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Data.Complex.BigOperators Mathlib.GroupTheory.GroupAction.Support Mathlib.Data.Multiset.Basic Mathlib.Algebra.Tropical.BigOperators Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Linear.Basic Mathlib.Data.TypeVec Mathlib.Data.Fintype.CardEmbedding Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Group.Basic Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Tactic.Linarith.Oracle.FourierMotzkin Mathlib.Data.Rat.Star Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.Algebra.Category.Grp.Preadditive Mathlib.SetTheory.Lists Mathlib.Data.Nat.Factorial.BigOperators Mathlib.Order.Category.FinBddDistLat Mathlib.Algebra.Regular.Pow Mathlib.CategoryTheory.Sites.Sheaf Mathlib.Algebra.Star.Rat Mathlib.Algebra.Star.NonUnitalSubsemiring Mathlib.Data.Finset.Order Mathlib.Algebra.Ring.BooleanRing Mathlib.Algebra.Order.Interval.Finset Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Tactic.MoveAdd Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Limits.Opposites Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.NumberTheory.Fermat Mathlib.SetTheory.Game.Impartial Mathlib.Algebra.Field.ULift Mathlib.Algebra.Order.Ring.Nat Mathlib.RingTheory.Congruence.Opposite Mathlib.CategoryTheory.Monoidal.Mon_ Mathlib.Computability.Language Mathlib.Data.NNRat.Lemmas Mathlib.Algebra.Order.Group.Action Mathlib.GroupTheory.GroupAction.Embedding Mathlib.Data.Fin.Fin2 Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.Data.Int.Cast.Basic Mathlib.Data.Finsupp.Fintype Mathlib.Algebra.Category.Ring.Basic Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Algebra.GroupWithZero.Divisibility Mathlib.Algebra.Order.Positive.Field Mathlib.Order.Interval.Set.IsoIoo Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Regular.SMul Mathlib.Data.Int.LeastGreatest Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.Tactic.NormNum.NatSqrt Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Data.Finsupp.Indicator Mathlib.Data.Fintype.Sigma Mathlib.Logic.Equiv.TransferInstance Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Algebra.Order.Ring.Cast Mathlib.Data.Nat.Choose.Sum Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory Mathlib.Algebra.Group.Opposite Mathlib.Data.Set.Sups Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.Data.DList.Instances Mathlib.Data.Int.Star Mathlib.Algebra.Order.Group.Int Mathlib.GroupTheory.GroupAction.Hom Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.GroupWithZero.NeZero Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Category.MonCat.Colimits Mathlib.Algebra.Group.Subgroup.Order Mathlib.Algebra.Order.Group.Prod Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence Mathlib.CategoryTheory.Limits.IsConnected Mathlib.GroupTheory.GroupAction.Ring Mathlib.Combinatorics.SimpleGraph.Path Mathlib.CategoryTheory.Limits.Comma Mathlib.Order.SupClosed Mathlib.Data.Sigma.Interval Mathlib.RepresentationTheory.Action.Limits Mathlib.Algebra.Ring.Prod Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts Mathlib.CategoryTheory.Shift.Induced Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.Algebra.EuclideanDomain.Defs Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.Data.PNat.Xgcd Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images Mathlib.Algebra.Ring.Divisibility.Basic Mathlib.CategoryTheory.Sites.Sheafification Mathlib.RingTheory.Nilpotent.Basic Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Monoidal.Limits Mathlib.Data.Finset.NatDivisors Mathlib.GroupTheory.Perm.Basic Mathlib.Algebra.BigOperators.Associated Mathlib.Data.Set.Pointwise.BigOperators Mathlib.CategoryTheory.Sites.Coverage Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.GroupTheory.Congruence.Basic Mathlib.Algebra.Group.UniqueProds.Basic Mathlib.Data.Sum.Interval Mathlib.Data.Fintype.Shrink Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.CategoryTheory.Limits.Final.ParallelPair Mathlib.Algebra.Group.Semiconj.Defs Mathlib.CategoryTheory.Limits.Filtered Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Testing.SlimCheck.Gen Mathlib.Algebra.Order.Ring.Canonical Mathlib.Data.Finite.Sigma Mathlib.Tactic.NormNum.Inv Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.CategoryTheory.Monoidal.Braided.Opposite Mathlib.Algebra.Ring.Idempotents Mathlib.Algebra.Homology.ShortComplex.QuasiIso Mathlib.Data.Finset.Fold Mathlib.CategoryTheory.Limits.Shapes.Countable Mathlib.Combinatorics.Young.YoungDiagram Mathlib.Data.List.EditDistance.Bounds Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.Algebra.Order.Ring.Int Mathlib.Algebra.Star.Conjneg Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Data.Nat.Factors Mathlib.Dynamics.BirkhoffSum.Basic Mathlib.CategoryTheory.Abelian.Subobject Mathlib.Data.PNat.Basic Mathlib.Tactic.Qify Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Internal.Limits Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory Mathlib.Algebra.Star.Center Mathlib.GroupTheory.Congruence.BigOperators Mathlib.Data.Part Mathlib.Tactic.FunProp.Attr Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.GroupWithZero.Pi Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.CategoryTheory.Simple Mathlib.Algebra.Order.Invertible Mathlib.Algebra.Order.UpperLower Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.CategoryTheory.Preadditive.Injective Mathlib.Tactic.Group Mathlib.CategoryTheory.SmallObject.Iteration Mathlib.CategoryTheory.Monoidal.Rigid.Braided Mathlib.CategoryTheory.Monoidal.Comon_ Mathlib.Data.Finite.Vector Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.CategoryTheory.Idempotents.Basic Mathlib.Logic.Small.Group Mathlib.Algebra.Order.Ring.Abs Mathlib.GroupTheory.Subgroup.Centralizer Mathlib.CategoryTheory.GradedObject.Trifunctor Mathlib.Algebra.PUnitInstances.Module Mathlib.Data.Fin.SuccPred Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq Mathlib.Data.Nat.Prime.Basic Mathlib.CategoryTheory.Abelian.Images Mathlib.CategoryTheory.Limits.Shapes.Reflexive Mathlib.CategoryTheory.Limits.ExactFunctor Mathlib.Deprecated.Group Mathlib.CategoryTheory.GuitartExact.VerticalComposition Mathlib.Data.Multiset.Fold Mathlib.Algebra.Group.Action.Basic Mathlib.Data.Finite.Powerset Mathlib.Algebra.CharZero.Defs Mathlib.Algebra.Order.Antidiag.Prod Mathlib.Data.Nat.Factorization.Root Mathlib.RingTheory.OreLocalization.Ring Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Computability.DFA Mathlib.Order.Interval.Finset.Defs Mathlib.Combinatorics.Young.SemistandardTableau Mathlib.Algebra.DirectSum.AddChar Mathlib.Data.Multiset.Range Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Tactic.NormNum.Eq Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Data.Fintype.List Mathlib.Algebra.Ring.Parity Mathlib.Data.Nat.Cast.Basic Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Data.Finsupp.Pointwise Mathlib.Algebra.Homology.SingleHomology Mathlib.AlgebraicTopology.SimplexCategory Mathlib.CategoryTheory.GradedObject Mathlib.NumberTheory.FactorisationProperties Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Closed.Types Mathlib.Data.Multiset.OrderedMonoid Mathlib.Data.Fin.Tuple.BubbleSortInduction Mathlib.Combinatorics.SetFamily.Shatter Mathlib.Algebra.Order.Hom.Monoid Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.Algebra.Order.Hom.Ring Mathlib.CategoryTheory.Sites.CoversTop Mathlib.Data.Finite.Set Mathlib.Logic.Small.Module Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Order.Group.Opposite Mathlib.CategoryTheory.Shift.SingleFunctors Mathlib.Algebra.Category.Ring.Limits Mathlib.Data.Finset.PImage Mathlib.Order.Filter.Curry Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.SetTheory.Game.PGame Mathlib.Algebra.BigOperators.Group.Multiset Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.Algebra.Order.Hom.Basic Mathlib.Data.Finset.Sort Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Data.Nat.Cast.Order.Basic Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.GroupWithZero.Pointwise.Finset Mathlib.CategoryTheory.Shift.Localization Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise Mathlib.Data.Rat.Cast.Lemmas Mathlib.CategoryTheory.Shift.CommShift Mathlib.RingTheory.LocalRing.Defs Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.Algebra.CharP.Pi Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Algebra.Ring.Ext Mathlib.Data.Finset.Card Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.CategoryTheory.Limits.Preserves.Filtered Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Algebra.FreeMonoid.Count Mathlib.Algebra.Order.Monoid.Canonical.Basic Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts Mathlib.Control.EquivFunctor.Instances Mathlib.Algebra.EuclideanDomain.Basic Mathlib.Algebra.Module.Pi Mathlib.CategoryTheory.GradedObject.Single Mathlib.CategoryTheory.FinCategory.AsType Mathlib.Tactic.ContinuousFunctionalCalculus Mathlib.CategoryTheory.Adjunction.Lifting.Left Mathlib.Algebra.Field.Power Mathlib.GroupTheory.GroupAction.IterateAct Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Data.Finsupp.BigOperators Mathlib.Data.Finset.Basic Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits Mathlib.Tactic.Measurability Mathlib.Topology.ContinuousMap.Defs Mathlib.GroupTheory.OreLocalization.Basic Mathlib.CategoryTheory.Filtered.Connected Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Algebra.Star.SelfAdjoint Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Cast.Synonym Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.Data.Vector.Basic Mathlib.Data.Fin.Tuple.Sort Mathlib.Data.Fintype.Prod Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Order.GameAdd Mathlib.AlgebraicTopology.SimplicialObject Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Tactic.Linarith.Parsing Mathlib.RingTheory.RingInvo Mathlib.Order.Partition.Finpartition Mathlib.Control.Fold Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.Order.Filter.Tendsto Mathlib.CategoryTheory.Limits.IndYoneda Mathlib.Order.SemiconjSup Mathlib.Algebra.BigOperators.Ring Mathlib.GroupTheory.GroupAction.Basic Mathlib.Algebra.Group.Fin.Basic Mathlib.Algebra.BigOperators.Group.List Mathlib.Algebra.Ring.Basic Mathlib.Data.Multiset.Sort Mathlib.Tactic.NormNum.OfScientific Mathlib.Data.ZMod.Defs Mathlib.Algebra.Order.Group.Cone Mathlib.Data.Set.Finite Mathlib.Algebra.Order.Field.Rat Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Star.Basic Mathlib.Data.Nat.Factorization.Basic Mathlib.Algebra.Group.FiniteSupport Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Order.Atoms.Finite Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.Hom.Defs Mathlib.CategoryTheory.Conj Mathlib.Tactic.NormNum.DivMod Mathlib.Computability.NFA Mathlib.Algebra.Order.Ring.Unbundled.Rat Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Algebra.Prod Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Order.Group.Defs Mathlib.RepresentationTheory.Action.Basic Mathlib.Algebra.PEmptyInstances Mathlib.Algebra.Order.AddTorsor Mathlib.Tactic.NoncommRing Mathlib.Algebra.Group.Subgroup.Basic Mathlib.Data.Finset.Union Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Tactic.ModCases Mathlib.Algebra.Group.Pointwise.Finset.Interval Mathlib.Algebra.Ring.Defs Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.CategoryTheory.Limits.Constructions.Equalizers Mathlib.CategoryTheory.GradedObject.Braiding Mathlib.CategoryTheory.Limits.Bicones Mathlib.Algebra.Order.Field.Defs Mathlib.Algebra.Order.Sum Mathlib.Order.Sublattice Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Order.Module.Pointwise Mathlib.Deprecated.Subring Mathlib.Algebra.Module.Prod Mathlib.CategoryTheory.GradedObject.Bifunctor Mathlib.CategoryTheory.GradedObject.Unitor Mathlib.CategoryTheory.Monoidal.Braided.Basic Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.Combinatorics.Additive.Corner.Defs Mathlib.Algebra.Order.GroupWithZero.Unbundled Mathlib.Order.Category.FinPartOrd Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Control.Functor.Multivariate Mathlib.Control.Traversable.Lemmas Mathlib.Algebra.GradedMulAction Mathlib.CategoryTheory.Abelian.Exact Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Order.SuccPred Mathlib.Tactic.Rify Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Monoidal.CommMon_ Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.GroupTheory.Subgroup.Simple Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Data.UInt Mathlib.Data.Int.CharZero Mathlib.Data.Sym.Card Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.Data.Multiset.Sections Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.Group.Commute.Basic Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Data.Finmap Mathlib.Order.Filter.Ring Mathlib.Combinatorics.SetFamily.LYM Mathlib.Tactic.Linarith.Datatypes Mathlib.Data.Sym.Sym2 Mathlib.Algebra.Module.Equiv.Defs Mathlib.Data.Finsupp.NeLocus Mathlib.Order.RelSeries Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.Algebra.Group.MinimalAxioms Mathlib.Tactic.FieldSimp Mathlib.Data.DFinsupp.Notation Mathlib.CategoryTheory.Sites.Over Mathlib.Computability.EpsilonNFA Mathlib.Algebra.Ring.Units Mathlib.Order.Interval.Finset.Box Mathlib.CategoryTheory.Subobject.Lattice Mathlib.Order.IsWellOrderLimitElement Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.Data.Finite.Sum Mathlib.Tactic.Ring.Compare Mathlib.Tactic.CancelDenoms.Core Mathlib.Data.Nat.PartENat Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.Order.KonigLemma Mathlib.Data.NNRat.Defs Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Ring.Center Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Algebra.Star.Subsemiring Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.Algebra.ContinuedFractions.Determinant Mathlib.Algebra.Group.Even Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Data.Nat.Choose.Multinomial Mathlib.Algebra.Ring.Action.Subobjects Mathlib.CategoryTheory.Monoidal.Types.Symmetric Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.RingTheory.Congruence.Basic Mathlib.Testing.SlimCheck.Testable Mathlib.Order.UpperLower.LocallyFinite Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Data.Nat.ChineseRemainder Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite Mathlib.Data.Rat.Cast.CharZero Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.Data.Fintype.Pi Mathlib.Data.Finset.Sigma Mathlib.Tactic.Positivity.Basic Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Monoidal.Discrete Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms Mathlib.Data.Vector.Snoc Mathlib.Combinatorics.SetFamily.Compression.Down Mathlib.Tactic.LinearCombination' Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Order.Group.PiLex Mathlib.Data.Fintype.Perm Mathlib.Tactic.Ring Mathlib.RingTheory.Coprime.Basic Mathlib.CategoryTheory.ConcreteCategory.Elementwise Mathlib.Combinatorics.Pigeonhole Mathlib.Algebra.CharZero.Infinite Mathlib.CategoryTheory.Limits.VanKampen Mathlib.Algebra.Module.PointwisePi Mathlib.Data.Nat.Cast.NeZero Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.Algebra.Field.Basic Mathlib.Data.Sign Mathlib.Data.Finsupp.Interval Mathlib.Tactic.Monotonicity.Lemmas Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts Mathlib.Algebra.GroupWithZero.Action.Pi Mathlib.Data.Rat.Sqrt Mathlib.Logic.Equiv.Fintype Mathlib.Algebra.Group.WithOne.Basic Mathlib.Algebra.BigOperators.GroupWithZero.Finset Mathlib.CategoryTheory.Generator Mathlib.Tactic.NormNum.IsCoprime Mathlib.Data.Fin.Tuple.Reflection Mathlib.CategoryTheory.Limits.Over Mathlib.Data.ENat.Lattice Mathlib.Algebra.Category.Grp.Biproducts Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.Data.Int.Cast.Lemmas Mathlib.Algebra.Module.LinearMap.Star Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.ExactSequence Mathlib.Data.Finset.Density Mathlib.CategoryTheory.Adjunction.Lifting.Right Mathlib.Data.Multiset.Fintype Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.GroupWithZero.Prod Mathlib.Algebra.Order.BigOperators.Group.Multiset Mathlib.Data.Real.Basic Mathlib.Algebra.Group.TypeTags Mathlib.Data.Fintype.Vector Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Data.Nat.Prime.Defs Mathlib.Tactic.NormNum.Pow Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Data.Real.Star Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.SetTheory.Cardinal.SchroederBernstein Mathlib.Data.Finset.NoncommProd Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Homology.Homotopy Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Group.Indicator Mathlib.Tactic.Abel Mathlib.Algebra.Order.Ring.Pow Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Algebra.Field.Subfield Mathlib.Algebra.Homology.CommSq Mathlib.Testing.SlimCheck.Sampleable Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Tactic.FunProp.Core Mathlib.CategoryTheory.ChosenFiniteProducts Mathlib.Data.List.Sym Mathlib.Algebra.Opposites Mathlib.Data.Nat.Choose.Bounds Mathlib.Data.Set.Pointwise.SMul Mathlib.Algebra.PUnitInstances.Algebra Mathlib.Data.Multiset.Pi Mathlib.CategoryTheory.Monad.Coequalizer Mathlib.Algebra.Algebra.Field Mathlib.GroupTheory.FreeGroup.Basic Mathlib.AlgebraicTopology.MooreComplex Mathlib.Data.Set.Pointwise.Finite Mathlib.Algebra.Order.Monoid.Prod Mathlib.Data.Finset.Preimage Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Data.Nat.PSub Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Algebra.GeomSum Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.Group.Units.Equiv Mathlib.CategoryTheory.Limits.Shapes.Biproducts Mathlib.Algebra.Associated.Basic Mathlib.Data.FunLike.Fintype Mathlib.Data.Complex.Basic Mathlib.Algebra.NoZeroSMulDivisors.Prod Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic Mathlib.Tactic.NormNum.Result Mathlib.Tactic.GCongr Mathlib.Order.Filter.NAry Mathlib.CategoryTheory.Closed.Zero Mathlib.Algebra.Order.Group.InjSurj Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory Mathlib.CategoryTheory.Closed.FunctorToTypes Mathlib.CategoryTheory.Limits.Lattice Mathlib.Algebra.Algebra.Defs Mathlib.Data.Nat.Cast.Commute Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.Data.List.Iterate Mathlib.Algebra.GroupWithZero.Hom Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.Combinatorics.Digraph.Basic Mathlib.Algebra.Homology.Augment Mathlib.Control.Bitraversable.Instances Mathlib.Data.Nat.Choose.Central Mathlib.Tactic.DeriveFintype Mathlib.Data.List.Prime Mathlib.CategoryTheory.Limits.FintypeCat Mathlib.CategoryTheory.Sites.Adjunction Mathlib.Data.Multiset.Powerset Mathlib.Algebra.Module.Defs Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.Limits.EpiMono Mathlib.Data.Int.Range Mathlib.CategoryTheory.Monoidal.Bimod Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Algebra.GroupWithZero.ULift Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.List.Pi Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Data.MLList.BestFirst Mathlib.Data.Finsupp.AList Mathlib.Algebra.BigOperators.WithTop Mathlib.Algebra.Order.Kleene Mathlib.GroupTheory.GroupAction.FixingSubgroup Mathlib.Deprecated.Subfield Mathlib.Algebra.GCDMonoid.Finset Mathlib.Algebra.Group.Ext Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.CategoryTheory.Closed.Cartesian Mathlib.Data.PNat.Interval Mathlib.Computability.RegularExpressions Mathlib.Algebra.BigOperators.NatAntidiagonal Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.Order.Filter.Extr Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.Algebra.Group.Action.Sum Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Order.Sub.Prod Mathlib.CategoryTheory.Linear.Yoneda Mathlib.Algebra.Group.Pi.Basic Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Module.Submodule.Order Mathlib.Algebra.Homology.HomologySequence Mathlib.Data.Nat.Lattice Mathlib.Algebra.Group.Support Mathlib.CategoryTheory.Shift.Basic Mathlib.Order.Filter.Prod Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Data.Finsupp.Order Mathlib.Algebra.Associated.OrderedCommMonoid Mathlib.CategoryTheory.Category.Grpd Mathlib.CategoryTheory.Limits.Preserves.Finite Mathlib.Data.Finset.NAry Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.Algebra.Order.Field.Pi Mathlib.GroupTheory.GroupAction.SubMulAction Mathlib.Algebra.Module.ULift Mathlib.Tactic.Linarith.Verification Mathlib.Algebra.Category.BoolRing Mathlib.Algebra.Ring.Nat Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.CategoryTheory.Groupoid.Subgroupoid Mathlib.Algebra.Order.Group.TypeTags Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers Mathlib.Order.PartialSups Mathlib.Tactic.Widget.GCongr Mathlib.Control.Traversable.Equiv Mathlib.Data.Nat.GCD.Basic Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Order.Ring.Rat Mathlib.Algebra.NoZeroSMulDivisors.Basic Mathlib.GroupTheory.NoncommCoprod Mathlib.Algebra.Order.Field.Canonical.Basic Mathlib.Order.Interval.Finset.Nat Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Star.CentroidHom Mathlib.Data.Int.ModEq Mathlib.Algebra.BigOperators.Expect Mathlib.Data.Int.Order.Units Mathlib.Algebra.Homology.ShortComplex.Limits Mathlib.Data.Ordmap.Ordnode Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Order.Monoid.Basic Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.Data.DFinsupp.Order Mathlib.Algebra.Order.Field.Subfield Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.Data.Set.Pointwise.BoundedMul Mathlib.Algebra.Order.Ring.Synonym Mathlib.Order.Filter.ListTraverse Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Data.Finite.Prod Mathlib.Tactic.SlimCheck Mathlib.CategoryTheory.Functor.Flat Mathlib.CategoryTheory.Monoidal.Conv Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.Combinatorics.Derangements.Finite Mathlib.RingTheory.OreLocalization.OreSet Mathlib.GroupTheory.Congruence.Defs Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.CategoryTheory.Limits.FunctorCategory.Finite Mathlib.Algebra.Module.Rat Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Order.AbsoluteValue Mathlib.Data.Nat.PrimeFin Mathlib.Data.Finset.Prod Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.ContinuedFractions.TerminatedStable Mathlib.Tactic.Linarith.Lemmas Mathlib.Tactic.DeriveTraversable Mathlib.Data.PNat.Factors Mathlib.Tactic.Bound Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Module.Submodule.Ker Mathlib.Data.Sym.Sym2.Order Mathlib.Tactic.Zify Mathlib.CategoryTheory.FinCategory.Basic Mathlib.Tactic.NormNum.GCD Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Limits.Final Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Subgroup.Actions Mathlib.CategoryTheory.Shift.Pullback Mathlib.Data.List.Cycle Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Rearrangement Mathlib.Algebra.GroupWithZero.Conj Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Algebra.Regular.Basic Mathlib.Combinatorics.Enumerative.Partition Mathlib.Order.CompletePartialOrder Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.Tactic.Peel Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Tactic.NormNum Mathlib.Data.List.ToFinsupp Mathlib.Algebra.BigOperators.Module Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.Field.IsField Mathlib.Control.Monad.Cont Mathlib.Algebra.Divisibility.Basic Mathlib.Algebra.Order.Ring.Cone Mathlib.Data.Int.SuccPred Mathlib.Algebra.GroupWithZero.Defs Mathlib.Order.KrullDimension Mathlib.Logic.Godel.GodelBetaFunction Mathlib.Algebra.Order.Group.Basic Mathlib.Data.Nat.MaxPowDiv Mathlib.Data.Multiset.Dedup Mathlib.Data.Int.GCD Mathlib.Data.Fintype.Lattice Mathlib.Algebra.Group.Action.Defs Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Algebra.Ring.Int Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Data.Multiset.Lattice Mathlib.Algebra.Order.Ring.Defs Mathlib.CategoryTheory.Functor.OfSequence Mathlib.Topology.Defs.Basic Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.CategoryTheory.Limits.Sifted Mathlib.Algebra.GroupPower.IterateHom Mathlib.Logic.Small.Ring Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.CategoryTheory.Limits.MonoCoprod Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.Algebra.Module.Hom Mathlib.Algebra.SMulWithZero
1

Declarations diff

- nsmulBinRec
- nsmulRec_eq_nsmulBinRec

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.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 18, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 18, 2024
…ro_iff` be `simp`

Also deprecate `Nat.bit_eq_zero`. It is identical to `Nat.bit_eq_zero_iff`.
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 20, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 20, 2024
@eric-wieser
Copy link
Member

We should check if the test from #17996 is impacted

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants