Commit 2024-08-15 08:47 7bf7fe19

View on Github →

chore: tidy various files (#15807)

Estimated changes

Modified Mathlib/Algebra/Category/Grp/EquivalenceGroupAddGroup.lean

Modified Mathlib/Algebra/Category/ModuleCat/Abelian.lean

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

Modified Mathlib/Algebra/Group/Semiconj/Units.lean

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Order/Archimedean/Hom.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

modified theorem InnerProductSpace.Core.inner_smul_ofReal_left

modified theorem InnerProductSpace.Core.inner_smul_ofReal_right

Modified Mathlib/Data/Finset/Image.lean

modified theorem Finset.disjoint_range_addLeftEmbedding

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

Modified Mathlib/ModelTheory/PartialEquiv.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

modified def MvPolynomial.msymm

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/Topology/Maps/Basic.lean