Commit 2024-04-24 11:33 dbc20eec

View on Github →

chore: tidy various files (#12316)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

added theorem WithZero.coe_le_iff

Modified Mathlib/Algebra/Order/Ring/Defs.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Analysis/Convex/Deriv.lean

Modified Mathlib/Analysis/NormedSpace/AddTorsor.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/Condensed/Equivalence.lean

Modified Mathlib/Data/Finsupp/Defs.lean

modified theorem AddEquiv.finsuppUnique_symm

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Submonoid/Inverses.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

Modified Mathlib/GroupTheory/Submonoid/Units.lean

modified theorem Subgroup.mem_of_mem_val_ofUnits

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

Modified Mathlib/Order/Filter/CardinalInter.lean

Modified Mathlib/Probability/Distributions/Uniform.lean