Commit 2024-01-22 18:51 8080f08c

View on Github →

chore: tidy various files (#9903)

Estimated changes

Modified Mathlib/Algebra/AddTorsor.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/CharP/ExpChar.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Hom.coe_ofLE

deleted theorem SimpleGraph.Hom.coe_ofLe

added def SimpleGraph.Hom.ofLE

deleted def SimpleGraph.Hom.ofLe

Modified Mathlib/Data/Fintype/Prod.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/Logic/Nonempty.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean