Commit 2023-03-27 05:33 0bcbc985

View on Github →

chore: tidy various files (#3110)

Estimated changes

Modified Mathlib/Algebra/Algebra/RestrictScalars.lean

added theorem RestrictScalars.smul_def

deleted theorem restrictScalars.smul_def

Modified Mathlib/Algebra/FreeAlgebra.lean

Modified Mathlib/Analysis/NormedSpace/MStructure.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/Control/LawfulFix.lean

modified def Part.toUnitMono

Modified Mathlib/Data/Finsupp/WellFounded.lean

Modified Mathlib/Data/MvPolynomial/Rename.lean

added theorem MvPolynomial.rename_prod_mk_eval₂

deleted theorem MvPolynomial.rename_prodmk_eval₂

Modified Mathlib/Data/Polynomial/DenomsClearable.lean

Modified Mathlib/Data/Tree.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

added theorem circleEquivGen_apply

added theorem circleEquivGen_symm_apply

deleted theorem circle_equiv_apply

deleted theorem circle_equiv_symm_apply

deleted theorem sq_ne_two_fin_zMod_four

added theorem sq_ne_two_fin_zmod_four

Modified Mathlib/NumberTheory/Zsqrtd/ToReal.lean

Modified Mathlib/RingTheory/Adjoin/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

added theorem MvPolynomial.IsSymmetric.C

deleted theorem MvPolynomial.IsSymmetric.c

modified def MvPolynomial.symmetricSubalgebra

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

modified theorem UniformSpace.Completion.smul_def