Commit 2023-07-18 03:34 bb6d52f7

View on Github →

chore: tidy various files (#5971)

Estimated changes

Modified Counterexamples/HomogeneousPrimeNotPrime.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Adjunctions.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Data/Int/GCD.lean

added theorem Nat.xgcdAux_P

added theorem Nat.xgcdAux_fst

added theorem Nat.xgcdAux_rec

added theorem Nat.xgcdAux_val

deleted theorem Nat.xgcd_aux_P

deleted theorem Nat.xgcd_aux_fst

deleted theorem Nat.xgcd_aux_rec

deleted theorem Nat.xgcd_aux_val

Modified Mathlib/GroupTheory/FiniteAbelian.lean

deleted theorem AddCommGroup.equiv_directSum_zMod_of_fintype

added theorem AddCommGroup.equiv_directSum_zmod_of_fintype

deleted theorem AddCommGroup.equiv_free_prod_directSum_zMod

added theorem AddCommGroup.equiv_free_prod_directSum_zmod

deleted theorem AddCommGroup.finite_of_fG_torsion

added theorem AddCommGroup.finite_of_fg_torsion

deleted theorem CommGroup.finite_of_fG_torsion

added theorem CommGroup.finite_of_fg_torsion

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/Order/Circular.lean

Modified Mathlib/SetTheory/Game/Short.lean

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified Mathlib/Topology/Algebra/Module/Alternating.lean