Commit 2025-06-02 07:15 492a63d1

View on Github →

chore: improve simp-set by putting hypotheses in simp normal form (#25024)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.Adj.adj_sub'

Modified Mathlib/Data/Finset/Image.lean

modified theorem List.toFinset_filterMap

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

modified theorem TangentBundle.trivializationAt_continuousLinearMapAt

modified theorem TangentBundle.trivializationAt_symmL

Modified Mathlib/Logic/Denumerable.lean

modified theorem Denumerable.ofNat_of_decode