Commit 2023-08-11 19:14 3697da16

View on Github →

chore: tidy various files (#6393)

Estimated changes

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

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/OfNorm.lean

deleted theorem InnerProductSpaceable.Inner_.conj_symm

deleted theorem InnerProductSpaceable.Inner_.norm_sq

added theorem InnerProductSpaceable.inner_.conj_symm

added theorem InnerProductSpaceable.inner_.norm_sq

Modified Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

modified theorem Complex.cpow_int_cast

modified theorem Complex.cpow_nat_cast

modified theorem Complex.cpow_nat_inv_pow

modified theorem Complex.cpow_two

modified theorem Complex.eq_zero_cpow_iff

modified theorem Complex.zero_cpow_eq_iff

Modified Mathlib/Data/ZMod/Defs.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem exists_contMDiffOn_forall_mem_convex_of_local

deleted theorem exists_cont_mdiff_forall_mem_convex_of_local

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

Modified Mathlib/Topology/VectorBundle/Hom.lean