Commit 2024-09-12 06:16 25ed3261

View on Github →

chore: remove some unnecessary haves (#16659) drive-by: convert some convert into exact.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/Data/Real/GoldenRatio.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/Order/Interval/Set/SurjOn.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

Modified test/ProdAssoc.lean